auto-generated structure projections not appearing

[fpvandoorn]

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

[hargoniX]

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]

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

[kmill]

Does docgen have some sort of aliasing system? For subobject projections and parent projections, we could alias them to the structure itself.

Aliases could help with #222 as well, where we'd look for all exported aliases (in the Lean sense) and add them as aliases in the docgen sense. Given a docgen alias name -> canonicalName, we'd have both name and canonicalName indexed, but only canonicalName would be included in the documentation itself.