to_additive documentation not rendered

Stream: mathlib4

[Emilie (Shad Amethyst)]

It took me a while to realize that there is an extensive documentation for how to_additive works at the bottom of its source file, but that same documentation is nowhere to be found on https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/ToAdditive.html#to_additive

Is there another place where that docstring is rendered?

[Jireh Loreaux]

In VS Code you can do #help attr to_additive to see that docstring.

[Jireh Loreaux]

@Floris van Doorn do we think this is the best place to put this documentation? I can't think of another place off-hand, but maybe it could just be copied into the module docstring so it appears in the docs?

[Jireh Loreaux]

@Emilie (Shad Amethyst) #help can give you lots of information like this.

[Emilie (Shad Amethyst)]

That's a nice thing to keep in mind. I usually jump straight to the online documentation, as similarly-useful theorems tend to float around what I was looking for

[Eric Wieser]

This sounds like something that should be fixed in doc-gen

[Kim Morrison]

In the meantime reproducing the text in the module docstring sounds like the best immediate plan. If doc-gen ever gets fixed it will be easy to deduplicate. @Emilie (Shad Amethyst), if you wanted to make a PR to that effect?

[Emilie (Shad Amethyst)]

I unfortunately won't be able to do that until wednesday. I'll certainly get to it then if I don't see a PR for it in the meantime :)

[Yury G. Kudryashov]

I think that we can definitely wait until Wednesday.

[Eric Wieser]

I suspect this is an easy fix in doc-gen4, and amounts to just not throwing away the declaration as auto-generated

[Jireh Loreaux]

Is it a declaration though? It's initializing an attribute.