leanprover-community/ProofWidgets4
feature request: widget to display the docstring of the current lemma
オープン
#70 opened on 2024/07/15
enhancementhelp wanted
Repository metrics
- Stars
- (219 個のスター)
- PR merge metrics
- (PR metrics pending)
説明
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.