Topic: instance priorities
Kevin Buzzard (Apr 02 2021 at 16:33):
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 (Apr 02 2021 at 16:36):
Oh thanks to Shing, who has just taught me how to answer such questions using grep.
Last updated: May 07 2021 at 12:15 UTC