list all attributes

Stream: lean4

[Asei Inoue]

For a particular identifier, is it possible to list all the attributes assigned to it?

For example, can it be verified that the [reducible] attribute is assigned to hoge when abbrev hoge := String?

[Kevin Buzzard]

Aah, I remember the old days...

This was a thing in lean 3 but apparently in lean 4 it's much harder.

[Kim Morrison]

Each attribute is responsible for storing its own data, and currently there is no central "registry" that attributes could, voluntarily or otherwise, contribute data to.

[Asei Inoue]

oh no..

[Asei Inoue]

So you're saying that no matter how hard we work on meta programming, we can't do it?

[Mario Carneiro]

The current limitation is that if you want to find out whether a definition has the reducible attribute, you have to query the reducible attribute extension. If you want to find out whether a definition has the csimp attribute you have to query the csimp extension (which has a different interface). And so on. This makes it exceedingly difficult to implement a version of #print that shows all attributes, because you have to write a hundred mini functions, and you won't be complete anyway because people can add more attributes later

[Mario Carneiro]

What we actually need here is to extend the interface of AttributeExtension such that it can print as well as parse attribute syntax

[Mario Carneiro]

and then you could just call all attribute extensions to print syntax for a given definition

[Mario Carneiro]

There is an RFC open for attributes in #print now: lean#6107 (and a fix in lean#6115)