leanprover/doc-gen4

Syntax declarations

hargoniX opened this issue · 0 comments

Syntax declarations are shown with their auto generated name as well as their parser as value right now. We could instead try pretty print the parser declaration and denote them explicitly as syntax with the proper syntax instead of a weird def that's just dangling around.