chore: remove simp from negOne_eq_allOnes (leanprover-community#665)

thorimur · Feb 20, 2024 · dd87fc3 · dd87fc3
1 parent 86d845f
commit dd87fc3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Std/Data/BitVec/Lemmas.lean b/Std/Data/BitVec/Lemmas.lean
@@ -249,7 +249,7 @@ private theorem allOnes_def :
   else
     simp [h]
 
-@[simp] theorem negOne_eq_allOnes : -1#w = allOnes w :=
+theorem negOne_eq_allOnes : -1#w = allOnes w :=
   rfl
 
 /-! ### or -/