From 32e2ec07baa7dee3a2e7d2b9d128156bffd21d89 Mon Sep 17 00:00:00 2001 From: Harun Khan <58151072+mhk119@users.noreply.github.com> Date: Sun, 27 Oct 2024 12:48:32 -0700 Subject: [PATCH] Update src/Init/Data/BitVec/Lemmas.lean Co-authored-by: Siddharth --- src/Init/Data/BitVec/Lemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 9bafc89460ec..e3dd1e87245b 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1536,8 +1536,8 @@ theorem toNat_signExtend_of_gt (x : BitVec w) {v : Nat} : (x.signExtend (w + v)).toNat = x.toNat + (2 ^ (w + v) - 2^w) * (if x.msb then 1 else 0) := by apply Nat.eq_of_testBit_eq intro i - rw [testBit_toNat, getLsbD_signExtend, Nat.pow_add, ← Nat.mul_sub_one] - rw [Nat.add_comm (x.toNat), Nat.mul_assoc, Nat.testBit_mul_pow_two_add _ (x.isLt)] + rw [testBit_toNat, getLsbD_signExtend, Nat.pow_add, ← Nat.mul_sub_one, + Nat.add_comm (x.toNat), Nat.mul_assoc, Nat.testBit_mul_pow_two_add _ (x.isLt)] by_cases h : i < w · simp [h, Nat.lt_add_right v h, testBit_toNat] · by_cases h2 : x.msb