How to inspect attributes?

Stream: lean4

[Josh Tilles]

Given some identifier, is it possible to view what (if any) attributes are associated with it?

XY explanation: I'm reviewing some old notes I made when learning Lean 3 and I'm trying to determine what still holds in Lean 4. In this particular case, I had written down "The command instance is syntax sugar for attribute [instance, reducible]."

[Mario Carneiro]

I don't think the instance command implies reducible

[Mario Carneiro]

it's just instance = @[instance] def

[Mario Carneiro]

But for your question, there is no uniform mechanism for determining the attributes on a declaration in lean 4. Each attribute stores its data in a custom data structure, which may or may not allow getting the information back out again. Some attributes have no permanent association at all and just do a thing when executed

[Kevin Buzzard]

In lean 3 this is just #print right?

[Mario Carneiro]

yes

[Mario Carneiro]

in lean 4 I think you won't ever see attributes in the output of #print

[Mario Carneiro]

actually from the code it looks like you can see @[reducible] and @[irreducible] but nothing else

[Mario Carneiro]

A general system for regurgitating attributes is still TODO I think

[Mario Carneiro]

my inclination is to have a registration mechanism where each new attribute adds a print plugin which allows print to query the attribute's state and reconstruct either a Syntax or MessageData object which will then be collated and used by #print