Zulip Chat Archive

Stream: new members

Topic: Additive documentation

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):


Rob Lewis (Jul 19 2020 at 11:17):

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

Last updated: Dec 20 2023 at 11:08 UTC