determine priority of instance

Stream: lean4

[Eric Wieser]

If I have a declaration Foo.toBar, how can I find out:

• Whether it is an instance?
• What the priority is if it is one?

In lean 3, the answer was #print Foo.toBar which would show all the attributes

[Jun Yoshida]

A little bit hacky, but the following does the trick:

#eval Lean.Meta.getInstancePriority? `Foo.toBar

[Eric Wieser]

Thanks! That was enough for me to me to open lean4#2905

[Kevin Buzzard]

Oh nice! It will be interesting to see a benchmark for how mathlib changes if this is indeed considered a bug and is fixed.