chore: delete double namespace BitVec.BitVec (#4165)

Fixes double namespace introduced in #4148
leanprover · May 14, 2024 · 367b978 · 367b978
1 parent f3538db
commit 367b978
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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]