doc for `notation`

Stream: lean4

[Michael Stoll]

Would it be possible to show some kind of docstring when hovering over notation? (Giving some explanation of the syntax and perhaps referring to Init.Notation for examples (the source code, the actual notation definitions do not show up on the HTML docs -- maybe this can be improved, too?)) Right now, exactly nothing happens when I move the mouse cursor on notation (in VSCode) in a .lean file.

[Mario Carneiro]

It will link to the source code for the notation parser, but only if you have it imported with import Lean

[Mario Carneiro]

The lack of documentation on commands is indeed a major issue. Unfortunately there aren't many people working on it, I've tried to do what I can but I don't have that much time to spend on it

[Mario Carneiro]

If you put /-- foo -/ docs on the syntax declaration it should show up in hovers (even if Lean is not imported). The problem is that no one put one on src#Lean.Parser.Command.notation