to_additive attributes

Stream: general

[Reid Barton]

      transform_decl_with_prefix_dict dict src tgt
        [`reducible, `simp, `instance, `refl, `symm, `trans, `elab_as_eliminator, `no_rsimp],

Can we make this list extensible? Maybe by ... giving these attributes an attribute?

[Yury G. Kudryashov]

Do you want to extend it outside of mathlib? If not, just as values here. AFAIR every read of an attribute comes at a price

[Yury G. Kudryashov]

@Gabriel Ebner am I right?

[Reid Barton]

In mathlib, but I don't want to create more dependencies if it's avoidable...

[Reid Barton]

I guess I could just create my attribute somewhere low in the hierarchy and then use it later

[Yury G. Kudryashov]

This is a list of names. They don't need to be defined at this point.

[Reid Barton]

Oh I see, I'm not used to this style but I guess it works.

[Yury G. Kudryashov]

If the code accidentally assumes that the attributes are defined, I can fix it tonight.

[Gabriel Ebner]

@Yury G. Kudryashov It's slow, but optimizable with a bit of effort. For "list of names", we can just copy the workaround used in the nolints attribute.

[Yury G. Kudryashov]

I'm afraid that I don't understand this workaround. Why exactly the new code is faster? Which call is slow and what is a fast alternative?

[Yury G. Kudryashov]

Is @[to_additive] slow for the same reason?