From e2816b7001bad98d4578ba7bbb096175381da559 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 23 Sep 2024 14:56:31 -0500 Subject: [PATCH] chore: remove unrelated change --- src/Init/Data/BitVec/Lemmas.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 616a3f90946a..de083f0523c3 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2248,6 +2248,7 @@ theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) := · simp [h] · rw [Nat.sub_add_cancel (Nat.two_pow_pos (w - 1)), Nat.two_pow_pred_mod_two_pow (by omega)] + /-! ### Non-overflow theorems -/ /--