Zulip Chat Archive

Stream: new members

Topic: Additive documentation


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jul 19 2020 at 10:47):

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

view this post on Zulip 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: May 08 2021 at 03:17 UTC