Zulip Chat Archive

Stream: new members

Topic: Failing to use a declared implicit variable


Stuart Presnell (Oct 14 2021 at 11:47):

I'm sure this is a simple thing I'm overlooking, but can someone explain why Lean is giving a don't know how to synthesize placeholder error at the theorem statement here, complaining that it needs a term of type A → B? Why isn't it using the implicit variable l : A → B declared above? (I thought I might need to explicitly include it to force Lean to notice it, but that hasn't fixed the problem).

import order.boolean_algebra

variables {A B : Type} [boolean_algebra A] [boolean_algebra B]
variables {l : A  B}

include l

def R (a:A) (b:B) : Prop := l a  b

theorem R_upward_closed_right (a:A) (b0 b1 : B) : (b0  b1)  (R a b0)  (R a b1)
  := sorry

omit l

Yaël Dillies (Oct 14 2021 at 12:43):

When you use R, l is treated as an implicit argument. Problem is, it doesn't appear in the definition of R, so Lean can't figure out what to put there!

Yaël Dillies (Oct 14 2021 at 12:45):

The definition of R doesn't "remember" that the particular variable it was defined with is l. You can achieve your expected result using parameter, but we advise against it.

Yaël Dillies (Oct 14 2021 at 12:45):

Best thing here is to simply make l explicit.

Stuart Presnell (Oct 14 2021 at 14:24):

Ok, thanks very much


Last updated: Dec 20 2023 at 11:08 UTC