Lemmy00's picture
Latest evaluator with explicit inference examples
1b6fcc6
Raw History Blame Contribute Delete
80 Bytes
import Mathlib
theorem nat_add_zero_identity (n : ℕ) : n + 0 = n := by
rfl