Open fpvandoorn opened 3 months ago
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.
That is fair. I don't actually feel strongly about seeing the declaration.
However, I think the following three things are important:
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
e.g.
CommMonoid.toMonoid
. These are useful to see (also in the instances forMonoid
).