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

[kmill]

leanprover/lean4#6704 has a possible fix for this. It modifies the app unexpanders for core notations, adding tags to tokens for the head constant.

@Komyyy's linked pull request solves this in a different way, by using heuristics that replace using pp.tagAppFns.

[Komyyy]

leanprover/lean4#6704 has a possible fix for this. It modifies the app unexpanders for core notations, adding tags to tokens for the head constant.

@Komyyy's linked pull request solves this in a different way, by using heuristics that replace using pp.tagAppFns.

This PR is closed because of some problems, leanprover/lean4#6704 will solve this issue.

[kmill]

https://leanprover-community.github.io/mathlib4_docs/Init/PropLemmas.html#exists_eq has a link now on the exists notation.

(App unexpanders in general now have links in their tokens.)