instance inference

Stream: new members

[Alex Zhang]

Am I able to block a built-in automatic instance inference in my own file?
for eg, block instance {α : Type*} : has_coe_to_sort (set α) := ⟨_, λ s, {x // x ∈ s}⟩

[Alex Zhang]

or block the attached simp to some built-in lemma in other files?

[Eric Wieser]

Why do you want to block that?

[Alex Zhang]

I just want to know whether Lean has this feature.
I only know I can add an attribute by attribute [] for a built-in lemma

[Eric Wieser]

local attribute [-instance] some_name

[Kyle Miller]

local attribute [-instance] set.has_coe_to_sort

Anonymous instances get names of this form. (They're not quite so anonymous as they first appear.)