Binder symbols in Exists is not linked

[eric-wieser]

Compare:

• Lean 4: exists_eq
• Lean 3: exists_eq

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]

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]

Yes, doc-gen shows whatever the info view shows