Additive documentation

Stream: new members

[Nicolò Cavalleri]

Suppose I have a structure with a @[to_additive] attribute such that the additive version is generated automatically. How can I edit the documentation of the additive version without restating it completely?

[Kenny Lau]

https://leanprover-community.github.io/mathlib_docs/commands.html#add_decl_doc

[Rob Lewis]

The to_additive command also takes an optional string to use as the doc string. https://leanprover-community.github.io/mathlib_docs/attributes.html#to_additive