docstring for commands only shown with import Lean
#3842
Comments
|
It seems that somehow the docstring needs to be added to |
|
The simplest fix there is to use an attribute IMO. But you could also try to derive the set of builtin parsers by traversing the definition of every |
github-merge-queue bot
pushed a commit
that referenced
this issue
Sep 13, 2024
This solves the issue where certain subexpressions are lacking syntax hovers because the hover text is not "builtin" - it only shows up if the `Parser` constant is imported in the environment. For top level syntaxes this is not a problem because `builtin_term_parser` will automatically add this doc information, but nested syntaxes don't get the same treatment. We could walk the expression and add builtin docs recursively, but this is somewhat expensive and unnecessary given that it's a fixed list of declarations in lean core. Moreover, there are reasons to want to control which syntax nodes actually get hovers, and while a better system for that is forthcoming, for now it can be achieved by strategically not applying the `@[builtin_doc]` attribute. Fixes #3842
tobiasgrosser
pushed a commit
to opencompl/lean4
that referenced
this issue
Sep 16, 2024
This solves the issue where certain subexpressions are lacking syntax hovers because the hover text is not "builtin" - it only shows up if the `Parser` constant is imported in the environment. For top level syntaxes this is not a problem because `builtin_term_parser` will automatically add this doc information, but nested syntaxes don't get the same treatment. We could walk the expression and add builtin docs recursively, but this is somewhat expensive and unnecessary given that it's a fixed list of declarations in lean core. Moreover, there are reasons to want to control which syntax nodes actually get hovers, and while a better system for that is forthcoming, for now it can be achieved by strategically not applying the `@[builtin_doc]` attribute. Fixes leanprover#3842
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Consider
There is no hover on
inductive. That’s unfortuante, because someone wrote a nice docstring for that syntax, as seen here.It does show up with
Maybe something has to be made built-in of sorts?
Versions
4.7.0
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: