From ea026463e7face8b8a458947717de2976942365e Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 19 Oct 2024 14:48:08 +0100 Subject: [PATCH] use implicit arguments --- 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 fa010ead49a0..2664a0fc4e71 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1980,7 +1980,7 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN @[simp] theorem toNat_sub {n} (x y : BitVec n) : (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl -@[simp, bv_toNat] theorem toInt_sub (x y : BitVec w) : +@[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, Int.natCast_sub (2 ^ w) y.toNat (by omega)]