From 3a1591df7e87abd5d0b7c45f1422da7dfc91956d Mon Sep 17 00:00:00 2001 From: Harun Khan <58151072+mhk119@users.noreply.github.com> Date: Tue, 12 Nov 2024 12:34:32 -0800 Subject: [PATCH] Update src/Init/Data/BitVec/Lemmas.lean Co-authored-by: Tobias Grosser --- 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 590149a7b02e..591a253c0438 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1253,7 +1253,7 @@ theorem ushiftRight_eq_zero (x : BitVec w) (n : Nat) (hn : w ≤ n) : Unsigned shift right by at least one bit makes the value of the bitvector less than or equal to `2^(w-1)`, makes the interpretation of the bitvector `Int` and `Nat` agree. -/ -theorem toInt_ushiftRight_pos_eq_toNat_shiftRight (x : BitVec w) (n : Nat) (hn : 0 < n) : +theorem toInt_ushiftRight_of_lt {x : BitVec w} {n : Nat} (hn : 0 < n) : (x >>> n).toInt = x.toNat >>> n := by rw [toInt_eq_toNat_cond] simp only [toNat_ushiftRight, ite_eq_left_iff, Nat.not_lt]