11 lines
384 B
Plaintext
11 lines
384 B
Plaintext
Solve the following problem with Lean 4 code and explanatory comments:
|
||
|
||
```lean4
|
||
import Mathlib
|
||
|
||
|
||
theorem demo (n : ℕ) : n + 0 = n := by sorry
|
||
```
|
||
|
||
Replace every sorry statement with an appropriate proof. Provide a complete solution in the lean4 code block, annotated with Lean 4 compiler feedback blocks in the form `/- <feedback> ... </feedback> -/` at the appropriate locations.
|