Synthesising Decidable.

Stream: lean4

[Wrenna Robson]

Suppose a proposition depending on a variable t has two instance of Decidable defined for it, but one of them depends on the typeclass [MyClass t] being availiable - it's more efficient, so essentially if it IS possible to use this instance for deciding the proposition, that is preferred. Will Lean automatically use the more-specific instance if it is available? Is there a way to make sure it does?

[Kenny Lau]

instance (priority := 100)

[Wrenna Robson]

On which one?

[Kenny Lau]

on the less specific one

[Wrenna Robson]

Great, thanks.

[François G. Dorais]

instance (priority := low) is more intuitive.