From 4f04112446a10ef996fdfed10e3991f2cafadc4a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 2 Sep 2024 16:34:56 +1000 Subject: [PATCH] chore: remove unused lemmas from a non-terminal simp (#5229) These non-terminal `simp` calls broke on a branch, but can be fixed on both `master` and that branch by removing a lemma. --- src/Lean/Data/HashMap.lean | 2 +- src/Lean/Data/HashSet.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean index 6cb6fa9fa4..609cd975fc 100644 --- a/src/Lean/Data/HashMap.lean +++ b/src/Lean/Data/HashMap.lean @@ -46,7 +46,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize if h' : u.toNat < sz then ⟨u, h'⟩ else - ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat, Fin.ofNat']; apply Nat.pos_of_isPowerOfTwo h⟩ + ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat]; apply Nat.pos_of_isPowerOfTwo h⟩ @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β := let ⟨i, h⟩ := mkIdx (hashFn a) data.property diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean index 30ff5814ff..cf6d67ebd0 100644 --- a/src/Lean/Data/HashSet.lean +++ b/src/Lean/Data/HashSet.lean @@ -43,7 +43,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize if h' : u.toNat < sz then ⟨u, h'⟩ else - ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat, Fin.ofNat']; apply Nat.pos_of_isPowerOfTwo h⟩ + ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat]; apply Nat.pos_of_isPowerOfTwo h⟩ @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α := let ⟨i, h⟩ := mkIdx (hashFn a) data.property