instance priorities

Stream: lean4

[Kevin Buzzard]

I've just been reading about default instances here. These default instances can have priorities. But does the concept of the priority of a generic instance exist in Lean 4? I'm idly porting logic.basic from Lean 3 to Lean 4 and this comes up near the start.

[Kevin Buzzard]

Oh thanks to Shing, who has just taught me how to answer such questions using grep.