Fix naming

opencompl · Sep 18, 2024 · 0c36ccf · 0c36ccf
1 parent 598f860
commit 0c36ccf
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -232,13 +232,13 @@ theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  b
 theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by
   decide
 
-@[simp] theorem ofBool_and : ofBool a &&& ofBool b = ofBool (a && b) := by
+@[simp] theorem and_ofBool : ofBool a &&& ofBool b = ofBool (a && b) := by
   cases a <;> cases b <;> rfl
 
-@[simp] theorem ofBool_or : ofBool a ||| ofBool b = ofBool (a || b) := by
+@[simp] theorem or_ofBool : ofBool a ||| ofBool b = ofBool (a || b) := by
   cases a <;> cases b <;> rfl
 
-@[simp] theorem ofBool_xor : ofBool a ^^^ ofBool b = ofBool (a ^^ b) := by
+@[simp] theorem xor_ofBool : ofBool a ^^^ ofBool b = ofBool (a ^^ b) := by
   cases a <;> cases b <;> rfl
 
 @[simp] theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by cases b <;> rfl