From 68250a972dbd5aeb3b29f86a1200124a1736eb2b Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Mon, 9 Dec 2024 16:10:56 -0800 Subject: [PATCH] small change --- 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 6b580f8c38c0..f93450e01d3f 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1494,7 +1494,7 @@ theorem getElem_sshiftRight {x : BitVec w} {s i : Nat} (h : i < w) : apply BitVec.lt_of_getLsbD hlsb ยท simp [sshiftRight_eq_of_msb_true hmsb] -theorem toInt_sshiftRight_of_pos {x : BitVec w} {n : Nat} : +theorem toInt_sshiftRight {x : BitVec w} {n : Nat} : (x.sshiftRight n).toInt = x.toInt >>> n := by match w with | 0 => simp [BitVec.sshiftRight, toInt_ofInt, Int.bmod_def, toInt_zero_length]