Can an attribute tell if it is applied to an instance?

Stream: lean4

[Eric Wieser]

In this mathlib PR, I ended up just checking if the name of the declaration starts with inst; can I do any better? The problem is that my attribute handler is running before the instance attribute handler, and so at the point I check the declaration has not been registered as an instance yet.

[Robin Arnez]

I don't think so but I don't think it would cause any problems if instance was appended to the start instead

[Floris van Doorn]

The instance attribute uses the default docs#Lean.AttributeApplicationTime, which is after type checking. One way to get simps to run after instance is to tell simps to apply after compilation (which, to be fair, is a bit of a hack).

[Floris van Doorn]

This is what we use in to_additive, IIRC to ensure that all equational lemmas have been generated.

[Eric Wieser]

I've updated #25125 to do that now, thanks for the tip