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.