Update src/Init/Data/BitVec/Lemmas.lean

Co-authored-by: Siddharth <[email protected]>
opencompl · May 28, 2024 · b1321e6 · b1321e6
1 parent 0a686ba
commit b1321e6
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
@@ -518,8 +518,8 @@ theorem and_assoc (a b c : BitVec w) :
 
 theorem xor_assoc (a b c : BitVec w) :
     a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := by
-  ext i; simp [Bool.xor_assoc]
-
+  ext i
+  simp [Bool.xor_assoc]
 /-! ### not -/
 
 theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl