Zulip Chat Archive

Stream: general

Topic: to_additive documentation


Eric Rodriguez (Nov 14 2021 at 11:46):

in here I raised the question about what is the standard for documentations of to_additive things - what has been done in the past?

Johan Commelin (Nov 16 2021 at 05:11):

I'm not sure if we have a consistent guideline here. I personally think that a remark along the lines of "The additive analogues are developed using to_additive." suffices in the module docstring.

Johan Commelin (Nov 16 2021 at 05:12):

cc @Julian Külshammer

Johan Commelin (Nov 16 2021 at 05:12):

Should we have a poll?

Julian Külshammer (Nov 16 2021 at 05:48):

I personally don't care either way and would also be fine with a poll. If I remember correctly, I did it like that already for group_theory order_of_element.lean

Yaël Dillies (Nov 16 2021 at 09:01):

I don't think it matters much. An allusion to to_additive in the module docstring is fine, copying everything between the additive and multiplicative version is fine.


Last updated: Dec 20 2023 at 11:08 UTC