fix: restore default BEq

Author: fgdorais

src/Init/Data/Bool.lean

@@ -12,19 +12,6 @@ public section
 
 namespace Bool
 
-/--
-Boolean “equality”. `beq x y` can be written `x == y`.
-
-`x == y` is `true` when `x = y`.  It is functionally the same as
-`decide (x = y)` but it uses non-branching code at runtime.
--/
-@[extern "lean_bool_dec_eq"]
-protected def beq (x y : Bool) : Bool := decide (x = y)
-
--- We override the default `BEq` so that it uses non-branching code at runtime.
-instance : BEq Bool := ⟨Bool.beq⟩
-instance : LawfulBEq Bool := ⟨of_decide_eq_true⟩
-
 /--
 Boolean “logical or”. `lor x y`.
 
@@ -75,7 +62,7 @@ Examples:
  * `true ^^ true = false`
 -/
 @[expose, reducible, extern "lean_bool_xor"]
-def xor (x y : Bool) : Bool := x != y
+def xor (x y : Bool) : Bool := bne x y
 
 @[inherit_doc] infixl:33 " ^^ " => Bool.xor
 

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -616,7 +616,7 @@ theorem or_mod_two_pow : (a ||| b) % 2 ^ n = a % 2 ^ n ||| b % 2 ^ n :=
 
 @[simp, grind =] theorem testBit_xor (x y i : Nat) :
     (x ^^^ y).testBit i = ((x.testBit i) ^^ (y.testBit i)) := by
-  simp [HXor.hXor, XorOp.xor, xor, testBit_bitwise ]
+  simp [HXor.hXor, XorOp.xor, xor, testBit_bitwise]
 
 @[simp, grind =] theorem zero_xor (x : Nat) : 0 ^^^ x = x := by
    apply Nat.eq_of_testBit_eq