From 514d0da1ab953391803db021f097bb752195912f Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 19 Oct 2024 12:08:35 +0100 Subject: [PATCH] Fix build --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index debaa26ad750..fa010ead49a0 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1982,7 +1982,7 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN @[simp, bv_toNat] theorem toInt_sub (x y : BitVec w) : (x - y).toInt = (x.toInt - y.toInt).bmod (2^w) := by - simp [toInt_eq_toNat_bmod] + simp [toInt_eq_toNat_bmod, Int.natCast_sub (2 ^ w) y.toNat (by omega)] -- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set. -- For reasons we don't yet understand, unfolding via `toNat_sub` sometimes