leanprover/doc-gen4

auto-generated structure projections not appearing

fpvandoorn opened this issue · 3 comments

fpvandoorn commented

e.g. CommMonoid.toMonoid.
These are useful to see (also in the instances for Monoid).

hargoniX commented

They're currently not printed on purpose as they do not exist in the code that is typed but are rather implicitly introduced by the extends thing (which is rendered). My current philosophy for how the docs should look like is "as close as possible to the original code" but if there are enough people that believe this should be different I'm happy to change it.

fpvandoorn commented

That is fair. I don't actually feel strongly about seeing the declaration.

However, I think the following three things are important:

  • Occurrences of CommMonoid.toMonoid in the doc should be a hyperlink to CommMonoid
  • CommMonoid.toMonoid should show up in the search results, linked to CommMonoid.
  • CommMonoid.toMonoid should be included in "computed" data, such as in the list of instances for Monoid.

EDIT:
And the following two links should jump to CommMonoid in the doc/source:
https://leanprover-community.github.io/mathlib4_docs/find/?pattern=CommMonoid.toMonoid#doc
https://leanprover-community.github.io/mathlib4_docs/find/?pattern=CommMonoid.toMonoid#src