Can't click on some docs

Stream: general

[Bolton Bailey]

docs#finSumFinEquiv_symm_last references docs#finSumFinEquiv, but there is no highlighted link.

[Bolton Bailey]

Where is the repo where I would report this bug

[Alex J. Best]

https://github.com/leanprover/doc-gen4, maybe this example can be added to https://github.com/leanprover/doc-gen4/issues/104

[Bolton Bailey]

Thanks, I was looking for it in the leanprover-community gh org with doc-gen (3).

[Henrik Böving]

No that's a different issue

[Bolton Bailey]

Actually this seems like a separate issue - in this case it is actually the code itself that is not linking

[Bolton Bailey]

Might be the up-arrow?

[Henrik Böving]

(up arrow is coercion) coercions do end up working here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Equiv/Fin.html#Equiv.piFinSucc_symm_apply but the expression is parenthesized. Very interesting. This is either an issue in the doc-gen4 linkifier but more likely an issue with Lean itself, I'll try to get the InfoTree from doc-gen and see which of the two are true

[Henrik Böving]

But please do open an issue about it so I don't forget^^

[Bolton Bailey]

https://github.com/leanprover/doc-gen4/issues/146