From 191f36caeb22eab2a1e0dbc2dad76b173a60121e Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 8 Nov 2024 15:55:33 +0000 Subject: [PATCH] chore: fixup proof after incorporating tobi suggestion --- 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 11cd308c3169..73c37df81b30 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2980,7 +2980,7 @@ theorem toInt_abs (x : BitVec w) : x.abs.toInt = if x = (intMin w) then (intMin w).toInt else x.toInt.abs := by rcases w with rfl | w · simp [toInt_zero_length] - · simp only [gt_iff_lt, Nat.zero_lt_succ, Nat.add_one_ne_zero, ↓reduceIte] + · simp only [toInt_intMin_eq_ite, gt_iff_lt, Nat.zero_lt_succ, Nat.add_one_ne_zero, ↓reduceIte] rw [BitVec.abs_eq_ite] by_cases hx : x = intMin (w + 1) · simp only [hx, reduceIte]