local attribute [instance]

Stream: new members

[Heather Macbeth]

Could someone help me troubleshoot this? I haven't used local attribute [instance] before, but I had thought the intended use case was precisely getting the below apply_instance to work.

import data.set.intervals
variables {α : Type*} [linear_order α] [densely_ordered α]
variables {a b : α} (h : a < b)
open set

noncomputable def Ioo_inhabited : inhabited (Ioo a b) :=
⟨classical.choice (nonempty.to_subtype (dense h))⟩

local attribute [instance, priority 5000] Ioo_inhabited

--fails
noncomputable example : inhabited (Ioo a b) := by apply_instance

--fails
noncomputable example : inhabited (Ioo a b) := by library_search

--works
noncomputable example : inhabited (Ioo a b) := Ioo_inhabited h

[Kenny Lau]

there are two problems with your code:

1. a < b is not a class, so Lean can't infer it
2. also you didn't include h so h isn't even in the context (try putting your cursor after by to see the context)

[Kenny Lau]

only unnamed instances are automatically included in the context

[Heather Macbeth]

Thanks! So how can I fix this? Do I want a local instance of fact with a < b?

[Sebastien Gouezel]

Yes. That's the way it's done in real_instances.lean.

[Heather Macbeth]

That's a great usage model. Thanks!