From bebf1927f84ee3e4b7d548a866479ac76baca41f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Jun 2023 20:35:33 -0700 Subject: [PATCH] chore: remove workarounds --- 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 4b2dfab2de..fed2405b7e 100644 --- a/src/Lean/Data/HashMap.lean +++ b/src/Lean/Data/HashMap.lean @@ -38,7 +38,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']; rw [Nat.zero_mod]; apply Nat.pos_of_isPowerOfTwo h⟩ + ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat, Fin.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 c266531e6d..70c1ebdc47 100644 --- a/src/Lean/Data/HashSet.lean +++ b/src/Lean/Data/HashSet.lean @@ -34,7 +34,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']; rw [Nat.zero_mod]; apply Nat.pos_of_isPowerOfTwo h⟩ + ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat, Fin.ofNat']; apply Nat.pos_of_isPowerOfTwo h⟩ @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α := let ⟨i, h⟩ := mkIdx (hashFn a) data.property