Zulip Chat Archive

Stream: lean4

Topic: Implicit arguments


Dan Velleman (Nov 26 2022 at 14:43):

This example works:

example (P : Nat  Prop) : ( {x : Nat}, P x)   {x : Nat}, P x := by
  intro h
  exact h

But this one doesn't:

example (P : Nat  Prop) : ( {x : Nat}, P x)   {x : Nat}, P x := by
  intro h
  have h2 : 0 = 0 := Eq.refl 0
  exact h

The exact h in the second example generates the error:

type mismatch
  h
has type
  P ?m.190 : Prop
but is expected to have type
   {x : Nat}, P x : Prop

In both examples, in the tactic state, both h and the goal are listed as ∀ {x : Nat}, P x, so it looks to a user like exact h should work. Examining the expressions for h and the goal, they are identical except that in the second example, the goal has mdata associated with it that says "noImplicitLambda". It is the introduction of h2 that causes that mdata to be attached to the goal, which explains why the first example works but the second doesn't.
Is this how it's supposed to work?


Last updated: Dec 20 2023 at 11:08 UTC