removed simp

leanprover · Sep 26, 2024 · 87df10f · 87df10f
1 parent eace028
commit 87df10f
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -1512,7 +1512,6 @@ theorem shiftRight_add {w : Nat} (x : BitVec w) (n m : Nat) :
   ext i
   simp [Nat.add_assoc n m i]
 
-@[simp]
 theorem shiftLeft_ushiftRight {x : BitVec w} {n : Nat}:
     x >>> n <<< n = x &&& BitVec.allOnes w <<< n := by
   induction n generalizing x