Search code examples
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.

    example : {x : nat // x = 0} :=
let x := 0 in ⟨x, rfl⟩

    In general have is usually used for proofs and let for everything else. In tactic mode you can use dsimp [x] to unfold the definition of let x := ...