From d0278ff12fd75697cde748bb3aeed5663adaf0dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 13 Sep 2024 11:25:13 +0200 Subject: [PATCH] recover prettier proof --- src/Init/Data/UInt/BasicAux.lean | 2 -- src/Std/Data/DHashMap/Internal/Index.lean | 7 +++---- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean index ed1cfb4bf9cf..f181e2645154 100644 --- a/src/Init/Data/UInt/BasicAux.lean +++ b/src/Init/Data/UInt/BasicAux.lean @@ -113,12 +113,10 @@ instance : Sub USize := ⟨USize.sub⟩ instance : LT USize := ⟨USize.lt⟩ instance : LE USize := ⟨USize.le⟩ -set_option bootstrap.genMatcherCode false in @[extern "lean_usize_dec_lt"] def USize.decLt (a b : USize) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec < b.toBitVec)) -set_option bootstrap.genMatcherCode false in @[extern "lean_usize_dec_le"] def USize.decLe (a b : USize) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec)) diff --git a/src/Std/Data/DHashMap/Internal/Index.lean b/src/Std/Data/DHashMap/Internal/Index.lean index 4f2d7be3ab7c..60e14072e767 100644 --- a/src/Std/Data/DHashMap/Internal/Index.lean +++ b/src/Std/Data/DHashMap/Internal/Index.lean @@ -56,10 +56,9 @@ cf. https://github.com/leanprover/lean4/issues/4157 · exact h' · rw [USize.le_def, BitVec.le_def] change _ ≤ (_ % _) - rw [Nat.mod_eq_of_lt h'] - rw [USize.toBitVec_eq_of_lt] - · omega - · cases usize_size_eq <;> omega + rw [Nat.mod_eq_of_lt h', USize.ofNat, BitVec.toNat_ofNat, Nat.mod_eq_of_lt] + · exact h + · exact Nat.lt_of_le_of_lt h h' · exact Nat.lt_of_lt_of_le (USize.toNat_lt_size _) (Nat.le_of_not_lt h')⟩ end Std.DHashMap.Internal