leanprover/doc-gen4

Linkifier to fields and constructors

fpvandoorn opened this issue 2 years ago · 0 comments

fpvandoorn commented 2 years ago

Fields of structures/classes and constructors of inductive types are not linked to correctly. Examples:

https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Nat.zero#doc
https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Group.toDivInvMonoid#doc