From 178d0ebe4f52db03311f4870379b0f85b2d0b57f Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 12 Nov 2022 21:08:06 -0500 Subject: [PATCH] fix: `protected` on `Nat.add_zero` --- src/Init/Core.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 6d7681f056..649fe3eb23 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -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