| have f := fun x => x * 2; | |
| have x := 1; | |
| have y := x + 1; | |
| f (y + x) : Nat | |
| a b : Nat | |
| h1 : a = 0 | |
| h2 : b = 0 | |
| ⊢ b < | |
| have x := 1; | |
| x + x | |
| (have this := id; | |
| this) | |
| 1 : Nat | |
| a b : Nat | |
| h : a > b | |
| ⊢ b < a | |
| have n := 5; | |
| ⟨[], ⋯⟩ : have n := 5; | |
| { as // as.length ≤ n } | |
| rfl : (have n := 5; | |
| n) = | |
| have n := 5; | |
| n | |
| rfl : 2 = 2 | |
| 5 | |
| have n := 5; | |
| n |