user-facing way to check attributes

Stream: lean4

[Eric Rodriguez]

How can I check if a specific declaration has a specific attribute without diving into meta? Is there something like #print attributes?

[Kim Morrison]

Unfortunately there is not a uniform mechanism: each attribute is free to manage its contents however it likess.

[Eric Rodriguez]

Coming back to this, I had a thought - what if there was an opt-(in/out) standardised way to do this? So that way we don't have to have _all_ attributes do this, but I think it is generally super helpful to check whether X attribute is on X lemma. This could've been useful in #10494, for example - we could've turned the manual checking that all the @[fun_prop] attributes were moved into a test file that guarantees that they are so tagged (and will remain that way in the future, unless changes are needed)

[Mario Carneiro]

I have had vague plans for this for some time, search "attribute delaborator" on this zulip, but nothing particularly concrete. It would have to be a new subsystem in core so probably best to have someone at the FRO on it, perhaps @Kyle Miller

[Mario Carneiro]

note that if you know the attribute you want to check in advance, this is usually not so hard, but as Scott says every attribute stores the data in a different way and there is no guarantee that you can recover what the original tagging was from the state