Zulip Chat Archive

Stream: new members

Topic: instance inference


Alex Zhang (Jul 17 2021 at 16:26):

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 (Jul 17 2021 at 16:33):

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

Eric Wieser (Jul 17 2021 at 16:52):

Why do you want to block that?

Alex Zhang (Jul 17 2021 at 16:58):

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 (Jul 17 2021 at 17:04):

local attribute [-instance] some_name

Kyle Miller (Jul 17 2021 at 17:05):

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.)


Last updated: Dec 20 2023 at 11:08 UTC