4 lines
63 B
Lean4
4 lines
63 B
Lean4
import Mathlib
|
||
|
||
theorem demo (n : ℕ) : n + 0 = n := by sorry
|
import Mathlib
|
||
|
||
theorem demo (n : ℕ) : n + 0 = n := by sorry
|