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

fix: protected on Nat.add_zero

Browse source
This commit is contained in:
Mario Carneiro 2022-11-12 21:08:06 -05:00 • committed by Leonardo de Moura
parent 7358df2f7e
commit 178d0ebe4f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Core.lean
View file

@ -457,7 +457,7 @@ inductive PNonScalar : Type u where
/-- You should not use this function -/
| mk (v : Nat) : PNonScalar
@[simp] theorem Nat.add_zero (n : Nat) : n + 0 = n := rfl
@[simp] protected theorem Nat.add_zero (n : Nat) : n + 0 = n := rfl
theorem optParam_eq (α : Sort u) (default : α) : optParam α default = α := rfl