get attributes on decl

Stream: metaprogramming / tactics

[Johan Commelin]

Given some environment e and a declaration d, how do you get all attributes on d?

[Scott Morrison]

I suspect you're going to have to come up with a list of all attributes, and check which ones point to d. :-(

[Mario Carneiro]

I just checked, and this is how #print works as well, it just goes through the list of all attributes and sees which ones d subscribes to

[Mario Carneiro]

unfortunately, the relevant function, get_attributes, is not exposed to lean

[Johan Commelin]

How hard would it be to expose it?