Data.Set.Pointwise.Basic (mathlib4#1188)

Stream: mathlib4

[Johan Commelin]

Here's another question about a mix of simp, to_additive and linting:
https://github.com/leanprover-community/mathlib4/pull/1188#discussion_r1065970851

[Johan Commelin]

My gut feeling is that Set.isUnit_iff should have a lower prio. Not sure how to pass that prio to to_additive.

[Floris van Doorn]

to_additive (attr := ...) supports all attribute syntax, so you can write to_additive (attr := simp 500), to_additive (attr := scoped simp), to_additive (attr := simp, nolint SimpNF), etc.

[Johan Commelin]

@Floris van Doorn now that you're here: what about deprecated?

[Johan Commelin]

to_additive (attr := deprecated which_name)?

[Johan Commelin]

Somehow we need to pass two alternative names: the multiplicative version and the additive version.

[Floris van Doorn]

In case you want to give different arguments to the attributes of multiplicative and additive declarations, just do it manually

@[to_additive, deprecated mulBar] def mulFoo ...
attribute [deprecated addBar] addFoo

[Floris van Doorn]

It seems not worth it to define custom syntax for that