From 367b97885a484a2e17e4cdade8dcd7fe05dbfb4c Mon Sep 17 00:00:00 2001 From: Siddharth Date: Tue, 14 May 2024 20:34:14 +0100 Subject: [PATCH] chore: delete double namespace BitVec.BitVec (#4165) Fixes double namespace introduced in #4148 --- 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 0ed05d4480..20886e33ac 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -609,7 +609,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} : (shiftLeftZeroExtend x i).msb = x.msb := by simp [shiftLeftZeroExtend_eq, BitVec.msb] -theorem BitVec.shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) : +theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) : (x <<< n) <<< m = x <<< (n + m) := by ext i simp only [getLsb_shiftLeft, Fin.is_lt, decide_True, Bool.true_and] @@ -705,7 +705,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} : simp only [getLsb_append, cond_eq_if] split <;> simp [*] -theorem BitVec.shiftRight_shiftRight (w : Nat) (x : BitVec w) (n m : Nat) : +theorem shiftRight_shiftRight (w : Nat) (x : BitVec w) (n m : Nat) : (x >>> n) >>> m = x >>> (n + m) := by ext i simp [Nat.add_assoc n m i]