Alias and to_additive

Stream: mathlib4

[Anatole Dedecker]

What is the correct way to mix to_additive and alias, in particular relative to the autogenerated documentation? I could add the "Alias of" text manually to the docstring of the additive version, but it should really be autogenerated...

[Anatole Dedecker]

Also, how does to_additive react to attr := deprecated some_mul_name? Will the additive version be registered as @[deprecated some_add_name]?

[Emilie (Shad Amethyst)]

I believe it should be, since parameters to attr are normally comma-separated

[Anatole Dedecker]

Yes, but the question is wether it additivizes the name that is passed as an argument to deprecated

[Ruben Van de Velde]

I just did

@[to_additive (attr := deprecated) AddMonoid.lcm_addOrder_eq_exponent] -- 2024-01-26
alias lcm_order_eq_exponent := lcm_orderOf_eq_exponent

which seemed to work

[Floris van Doorn]

Anatole Dedecker said:

Yes, but the question is wether it additivizes the name that is passed as an argument to deprecated

Arguments given to the deprecated attribute are not additivized, no. Just add the attribute [deprecated ...] afterwards.

[Ruben Van de Velde]

Oh, that's annoying. Would it be hard to make this "just work(TM)"?

[Floris van Doorn]

to_additive already uses a bunch of hacks to make it interact nicely with some common other attributes. It is indeed hard to make this work properly without redesigning the whole attribute system. We could add an additional hack to make it work specifically with the deprecated tactic, but I don't think that is the way to go.