## Stream: new members

#### Nicolò Cavalleri (Jul 19 2020 at 10:42):

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 (Jul 19 2020 at 10:47):

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