From d10e3da6738dfd9435e571fa9526360611bef582 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Wed, 19 Jul 2023 00:36:54 -0400 Subject: [PATCH] fix: protect sizeOf lemmas --- src/Init/SizeOfLemmas.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Init/SizeOfLemmas.lean b/src/Init/SizeOfLemmas.lean index 3c57afabef..4fbda63e56 100644 --- a/src/Init/SizeOfLemmas.lean +++ b/src/Init/SizeOfLemmas.lean @@ -8,26 +8,26 @@ import Init.Meta import Init.SizeOf import Init.Data.Nat.Linear -@[simp] theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by +@[simp] protected theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by cases a; simp_arith -@[simp] theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 2 := by +@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 2 := by cases a; simp_arith [UInt8.toNat] -@[simp] theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 2 := by +@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 2 := by cases a; simp_arith [UInt16.toNat] -@[simp] theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 2 := by +@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 2 := by cases a; simp_arith [UInt32.toNat] -@[simp] theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 2 := by +@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 2 := by cases a; simp_arith [UInt64.toNat] -@[simp] theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 2 := by +@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 2 := by cases a; simp_arith [USize.toNat] -@[simp] theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 3 := by +@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 3 := by cases a; simp_arith [Char.toNat] -@[simp] theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by +@[simp] protected theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by cases s; simp_arith