Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feature request: widget to display the docstring of the current lemma #70

Open
Vtec234 opened this issue Jul 15, 2024 · 0 comments
Open
Labels
enhancement New feature or request help wanted Extra attention is needed

Comments

@Vtec234
Copy link
Collaborator

Vtec234 commented Jul 15, 2024

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.

@Vtec234 Vtec234 added enhancement New feature or request help wanted Extra attention is needed labels Jul 15, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request help wanted Extra attention is needed
Projects
None yet
Development

No branches or pull requests

1 participant