how to check attribute

Stream: Is there code for X?

[Asei Inoue]

@[ext] structure Point (α : Type) where
  x : α
  y : α

#check Point.ext

-- how to check `Point.ext` has attribute `ext`?
-- `Point.ext` is just an example; in general, I want to check whether an attribute is present or not.

[Kyle Miller]

Do you want a command to run as a user to check this? or are you looking for checking this programmatically in a metaprogram?

For the first, there's no pre-existing solution. I eventually want #print Point to list the attributes associated to Point.

[Asei Inoue]

Do you want a command to run as a user to check this? or are you looking for checking this programmatically in a metaprogram?

The latter, I guess.

[Asei Inoue]

It would be nice to have a built-in command like #synth.