lean

Difference between let and have keywords in lean 4

I noticed that both

#eval have x : Nat := 3 ; x*2

and

#eval let x : Nat := 3 ; x*2

work in the same way. Same goes when proving theorems. Are those equivalent? What is the difference between them?

Solution

  • The difference is that let "remembers" the definition and have forgets it.

    So for example, the following works with let but not have in Lean 4.

    example : {x : Nat // x = 0} := let x := 0 ; ⟨x, rfl⟩

    In general have is usually used for proofs and let for everything else. In Lean3 tactic mode you can use dsimp [x] to unfold the definition of let x := ..., I'm not sure how to do this in Lean4.