28 lines
523 B
Plaintext
28 lines
523 B
Plaintext
|
Here is the complete Lean 4 proof annotated with Lean 4 compiler feedback blocks:
|
|||
|
|
|
|||
|
|
```lean4
|
|||
|
|
import Mathlib
|
|||
|
|
|
|||
|
|
-- Theorem: For any natural number n, n + 0 = n.
|
|||
|
|
theorem demo (n : ℕ) : n + 0 = n := by
|
|||
|
|
/- <feedback>
|
|||
|
|
-- proof state:
|
|||
|
|
n : ℕ
|
|||
|
|
⊢ n + 0 = n
|
|||
|
|
</feedback> -/
|
|||
|
|
induction n with
|
|||
|
|
/- <feedback>
|
|||
|
|
-- proof state:
|
|||
|
|
case zero
|
|||
|
|
⊢ 0 + 0 = 0
|
|||
|
|
</feedback> -/
|
|||
|
|
| zero => rfl
|
|||
|
|
/- <feedback>
|
|||
|
|
-- proof state:
|
|||
|
|
ih : n + 0 = n
|
|||
|
|
case succ
|
|||
|
|
⊢ n + 1 + 0 = n + 1
|
|||
|
|
</feedback> -/
|
|||
|
|
| succ n ih => simp_all
|
|||
|
|
```
|