search

leanprover / doc-gen4

Document Generator for Lean 4
Apache License 2.0
67 stars 42 forks source link

Binder symbols in Exists is not linked #91

Open eric-wieser opened 2 years ago

eric-wieser commented 2 years ago

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 https://github.com/leanprover-community/lean/pull/781.

hargoniX commented 2 years ago

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 2 years ago

Yes, doc-gen shows whatever the info view shows