leanprover-community/ProofWidgets4
feature request: widget to display the docstring of the current lemma
開放
#70 建立於 2024年7月15日
enhancementhelp wanted
倉庫指標
- 星標
- (219 顆星)
- PR 合併指標
- (PR 指標待抓取)
描述
For interactive proof it can be helpful to have the docstring for the lemma currently being proven pretty-printed in the infoview alongside the tactic state. This can be especially useful when the docstring includes sources for TikZ diagrams. These should be rendered correctly in the infoview.