Dynamically changing instance priorities

Stream: lean4

[Tomaz Gomes]

In Lean 3, we could do something like:

local attribute [instance, priority 10] prop_decidable

to reassign the priority of an instance just inside a single file. Is it possible to do something like that in Lean 4?

[Eric Wieser]

Is that the specific instance you care about, or just an example?

[Eric Wieser]

If the former, then that's what the Classical scope is for in mathlib

[Tomaz Gomes]

Actually I wanted to do the opposite, that is elevate the priority of propDecidable... I suppose that I could do that by using the same function as the classical tactic uses (Meta.addInstance)? But that works just inside a proof, I wanted to do that in the whole file