max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/data/nat/lemmas): mark nat.add_zero as protected

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-07 14:17:56 -08:00
parent 0c4c41ae54
commit f56250d41e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/data/nat/lemmas.lean
View file

@ -20,7 +20,7 @@ lemma succ_add : ∀ n m : ℕ, (succ n) + m = succ (n + m)
lemma add_succ : ∀ n m : ℕ, n + succ m = succ (n + m) :=
λ n m, rfl
lemma add_zero : ∀ n : ℕ, n + 0 = n :=
protected lemma add_zero : ∀ n : ℕ, n + 0 = n :=
λ n, rfl
lemma add_one_eq_succ : ∀ n : ℕ, n + 1 = succ n :=