Zulip Chat Archive

Stream: new members

Topic: local attribute [instance]


view this post on Zulip Heather Macbeth (Sep 03 2020 at 05:41):

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

view this post on Zulip Kenny Lau (Sep 03 2020 at 05:45):

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)

view this post on Zulip Kenny Lau (Sep 03 2020 at 05:45):

only unnamed instances are automatically included in the context

view this post on Zulip Heather Macbeth (Sep 03 2020 at 05:51):

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

view this post on Zulip Sebastien Gouezel (Sep 03 2020 at 05:58):

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

view this post on Zulip Heather Macbeth (Sep 03 2020 at 06:00):

That's a great usage model. Thanks!


Last updated: May 13 2021 at 21:12 UTC