Binder symbols in Exists is not linked
eric-wieser opened this issue · 2 comments
eric-wieser commented
Compare:
Only the Lean3 versions let you inspect the binder symbol in the docs. While for Existss this is obvious, for other binders the hover text is very useful.
It's possible this requires a patch to Lean4 itself; the Lean 3 patch was leanprover-community/lean#781.
hargoniX commented
This does most likely require a patch to lean itself, doc-gen4 merely analyses datastructures on top of the info trees: https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Output/Base.lean#L208
CC: @Kha what do you think?
Kha commented
Yes, doc-gen shows whatever the info view shows