fix

fix test

src/Init/Data/BitVec/Bitblast.lean

@@ -132,7 +132,7 @@ theorem toNat_add_of_and_eq_zero {x y : BitVec w} (h : x &&& y = 0#w) :
   simp [not_eq_true, carry_of_and_eq_zero h]
 
 /-- Carry function for bitwise addition. -/
-def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, Bool.xor x (Bool.xor y c))
+def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, x ^^ (y ^^ c))
 
 /-- Bitwise addition implemented via a ripple carry adder. -/
 def adc (x y : BitVec w) : Bool → Bool × BitVec w :=
@@ -140,7 +140,7 @@ def adc (x y : BitVec w) : Bool → Bool × BitVec w :=
 
 theorem getLsbD_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
     getLsbD (x + y + setWidth w (ofBool c)) i =
-      Bool.xor (getLsbD x i) (Bool.xor (getLsbD y i) (carry i x y c)) := by
+      (getLsbD x i ^^ (getLsbD y i ^^ carry i x y c)) := by
   let ⟨x, x_lt⟩ := x
   let ⟨y, y_lt⟩ := y
   simp only [getLsbD, toNat_add, toNat_setWidth, i_lt, toNat_ofFin, toNat_ofBool,
@@ -161,7 +161,7 @@ theorem getLsbD_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool
 
 theorem getLsbD_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
     getLsbD (x + y) i =
-      Bool.xor (getLsbD x i) (Bool.xor (getLsbD y i) (carry i x y false)) := by
+      (getLsbD x i ^^ (getLsbD y i ^^ carry i x y false)) := by
   simpa using getLsbD_add_add_bool i_lt x y false
 
 theorem adc_spec (x y : BitVec w) (c : Bool) :

src/Init/Data/BitVec/Lemmas.lean

@@ -752,20 +752,20 @@ instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_co
   exact (Nat.mod_eq_of_lt <| Nat.xor_lt_two_pow x.isLt y.isLt).symm
 
 @[simp] theorem getLsbD_xor {x y : BitVec v} :
-    (x ^^^ y).getLsbD i = (xor (x.getLsbD i) (y.getLsbD i)) := by
+    (x ^^^ y).getLsbD i = ((x.getLsbD i) ^^ (y.getLsbD i)) := by
   rw [← testBit_toNat, getLsbD, getLsbD]
   simp
 
 @[simp] theorem getMsbD_xor {x y : BitVec w} :
-    (x ^^^ y).getMsbD i = (xor (x.getMsbD i) (y.getMsbD i)) := by
+    (x ^^^ y).getMsbD i = (x.getMsbD i ^^ y.getMsbD i) := by
   simp only [getMsbD]
   by_cases h : i < w <;> simp [h]
 
-@[simp] theorem getElem_xor {x y : BitVec w} {i : Nat} (h : i < w) : (x ^^^ y)[i] = (xor x[i] y[i]) := by
+@[simp] theorem getElem_xor {x y : BitVec w} {i : Nat} (h : i < w) : (x ^^^ y)[i] = (x[i] ^^ y[i]) := by
   simp [getElem_eq_testBit_toNat]
 
 @[simp] theorem msb_xor {x y : BitVec w} :
-    (x ^^^ y).msb = (xor x.msb y.msb) := by
+    (x ^^^ y).msb = (x.msb ^^ y.msb) := by
   simp [BitVec.msb]
 
 @[simp] theorem setWidth_xor {x y : BitVec w} :
@@ -1427,7 +1427,7 @@ theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)
   ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
 
 @[simp] theorem cons_xor_cons (x y : BitVec w) (a b : Bool) :
-    (cons a x) ^^^ (cons b y) = cons (xor a b) (x ^^^ y) := by
+    (cons a x) ^^^ (cons b y) = cons (a ^^ b) (x ^^^ y) := by
   ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
 
 /-! ### concat -/
@@ -1466,7 +1466,7 @@ theorem getLsbD_concat (x : BitVec w) (b : Bool) (i : Nat) :
   ext i; cases i using Fin.succRecOn <;> simp
 
 @[simp] theorem concat_xor_concat (x y : BitVec w) (a b : Bool) :
-    (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (xor a b) := by
+    (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (a ^^ b) := by
   ext i; cases i using Fin.succRecOn <;> simp
 
 /-! ### add -/

src/Init/Data/Bool.lean

@@ -12,6 +12,8 @@ namespace Bool
 /-- Boolean exclusive or -/
 abbrev xor : Bool → Bool → Bool := bne
 
+@[inherit_doc] infixl:33 " ^^ " => xor
+
 instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∀ x, p x) :=
   match inst true, inst false with
   | isFalse ht, _ => isFalse fun h => absurd (h _) ht
@@ -145,8 +147,8 @@ theorem and_or_distrib_right : ∀ (x y z : Bool), ((x || y) && z) = (x && z ||
 theorem or_and_distrib_left  : ∀ (x y z : Bool), (x || y && z) = ((x || y) && (x || z)) := by decide
 theorem or_and_distrib_right : ∀ (x y z : Bool), (x && y || z) = ((x || z) && (y || z)) := by decide
 
-theorem and_xor_distrib_left  : ∀ (x y z : Bool), (x && xor y z) = xor (x && y) (x && z) := by decide
-theorem and_xor_distrib_right : ∀ (x y z : Bool), (xor x y && z) = xor (x && z) (y && z) := by decide
+theorem and_xor_distrib_left  : ∀ (x y z : Bool), (x && (y ^^ z)) = ((x && y) ^^ (x && z)) := by decide
+theorem and_xor_distrib_right : ∀ (x y z : Bool), ((x ^^ y) && z) = ((x && z) ^^ (y && z)) := by decide
 
 /-- De Morgan's law for boolean and -/
 @[simp] theorem not_and : ∀ (x y : Bool), (!(x && y)) = (!x || !y) := by decide
@@ -274,37 +276,37 @@ theorem beq_comm {α} [BEq α] [LawfulBEq α] {a b : α} : (a == b) = (b == a) :
 
 /-! ### xor -/
 
-theorem false_xor : ∀ (x : Bool), xor false x = x := false_bne
+theorem false_xor : ∀ (x : Bool), (false ^^ x) = x := false_bne
 
-theorem xor_false : ∀ (x : Bool), xor x false = x := bne_false
+theorem xor_false : ∀ (x : Bool), (x ^^ false) = x := bne_false
 
-theorem true_xor : ∀ (x : Bool), xor true x = !x := true_bne
+theorem true_xor : ∀ (x : Bool), (true ^^ x) = !x := true_bne
 
-theorem xor_true : ∀ (x : Bool), xor x true = !x := bne_true
+theorem xor_true : ∀ (x : Bool), (x ^^ true) = !x := bne_true
 
-theorem not_xor_self : ∀ (x : Bool), xor (!x) x = true := not_bne_self
+theorem not_xor_self : ∀ (x : Bool), (!x ^^ x) = true := not_bne_self
 
-theorem xor_not_self : ∀ (x : Bool), xor x (!x) = true := bne_not_self
+theorem xor_not_self : ∀ (x : Bool), (x ^^ !x) = true := bne_not_self
 
-theorem not_xor : ∀ (x y : Bool), xor (!x) y = !(xor x y) := by decide
+theorem not_xor : ∀ (x y : Bool), (!x ^^ y) = !(x ^^ y) := by decide
 
-theorem xor_not : ∀ (x y : Bool), xor x (!y) = !(xor x y) := by decide
+theorem xor_not : ∀ (x y : Bool), (x ^^ !y) = !(x ^^ y) := by decide
 
-theorem not_xor_not : ∀ (x y : Bool), xor (!x) (!y) = (xor x y) := not_bne_not
+theorem not_xor_not : ∀ (x y : Bool), (!x ^^ !y) = (x ^^ y) := not_bne_not
 
-theorem xor_self : ∀ (x : Bool), xor x x = false := by decide
+theorem xor_self : ∀ (x : Bool), (x ^^ x) = false := by decide
 
-theorem xor_comm : ∀ (x y : Bool), xor x y = xor y x := by decide
+theorem xor_comm : ∀ (x y : Bool), (x ^^ y) = (y ^^ x) := by decide
 
-theorem xor_left_comm : ∀ (x y z : Bool), xor x (xor y z) = xor y (xor x z) := by decide
+theorem xor_left_comm : ∀ (x y z : Bool), (x ^^ (y ^^ z)) = (y ^^ (x ^^ z)) := by decide
 
-theorem xor_right_comm : ∀ (x y z : Bool), xor (xor x y) z = xor (xor x z) y := by decide
+theorem xor_right_comm : ∀ (x y z : Bool), ((x ^^ y) ^^ z) = ((x ^^ z) ^^ y) := by decide
 
-theorem xor_assoc : ∀ (x y z : Bool), xor (xor x y) z = xor x (xor y z) := bne_assoc
+theorem xor_assoc : ∀ (x y z : Bool), ((x ^^ y) ^^ z) = (x ^^ (y ^^ z)) := bne_assoc
 
-theorem xor_left_inj : ∀ {x y z : Bool}, xor x y = xor x z ↔ y = z := bne_left_inj
+theorem xor_left_inj : ∀ {x y z : Bool}, (x ^^ y) = (x ^^ z) ↔ y = z := bne_left_inj
 
-theorem xor_right_inj : ∀ {x y z : Bool}, xor x z = xor y z ↔ x = y := bne_right_inj
+theorem xor_right_inj : ∀ {x y z : Bool}, (x ^^ z) = (y ^^ z) ↔ x = y := bne_right_inj
 
 /-! ### le/lt -/
 

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

@@ -237,7 +237,7 @@ theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = !(testBit x i
   | _ p => simp [p]
 
 theorem testBit_mul_two_pow_add_eq (a b i : Nat) :
-    testBit (2^i*a + b) i = Bool.xor (a%2 = 1) (testBit b i) := by
+    testBit (2^i*a + b) i = (a%2 = 1 ^^ testBit b i) := by
   match a with
   | 0 => simp
   | a+1 =>
@@ -570,7 +570,7 @@ theorem or_div_two : (a ||| b) / 2 = a / 2 ||| b / 2 := by
 /-! ### xor -/
 
 @[simp] theorem testBit_xor (x y i : Nat) :
-    (x ^^^ y).testBit i = Bool.xor (x.testBit i) (y.testBit i) := by
+    (x ^^^ y).testBit i = ((x.testBit i) ^^ (y.testBit i)) := by
   simp [HXor.hXor, Xor.xor, xor, testBit_bitwise ]
 
 @[simp] theorem zero_xor (x : Nat) : 0 ^^^ x = x := by

src/Std/Sat/AIG/CNF.lean

@@ -67,7 +67,7 @@ theorem atomToCNF_eval :
 theorem gateToCNF_eval :
     (gateToCNF output lhs rhs linv rinv).eval assign
       =
-    (assign output == ((xor (assign lhs) linv) && (xor (assign rhs) rinv))) := by
+    (assign output == (((assign lhs) ^^ linv) && ((assign rhs) ^^ rinv))) := by
   simp only [CNF.eval, gateToCNF, CNF.Clause.eval, List.all_cons, List.any_cons, beq_false,
     List.any_nil, Bool.or_false, beq_true, List.all_nil, Bool.and_true]
   cases assign output

src/Std/Sat/AIG/CachedGatesLemmas.lean

@@ -32,7 +32,7 @@ private theorem or_as_aig : ∀ (a b : Bool), (!(!a && !b)) = (a || b) := by
 /--
 Encoding of XOR as boolean expression in AIG form.
 -/
-private theorem xor_as_aig : ∀ (a b : Bool), (!(a && b) && !(!a && !b)) = (xor a b) := by
+private theorem xor_as_aig : ∀ (a b : Bool), (!(a && b) && !(!a && !b)) = (a ^^ b) := by
   decide
 
 /--

src/Std/Sat/AIG/Lemmas.lean

@@ -92,11 +92,7 @@ instance : LawfulOperator α GateInput mkGate where
 theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
     ⟦aig.mkGate input, assign⟧
       =
-    (
-      (xor ⟦aig, input.lhs.ref, assign⟧ input.lhs.inv)
-        &&
-      (xor ⟦aig, input.rhs.ref, assign⟧ input.rhs.inv)
-    ) := by
+    ((⟦aig, input.lhs.ref, assign⟧ ^^ input.lhs.inv) && (⟦aig, input.rhs.ref, assign⟧ ^^ input.rhs.inv)) := by
   conv =>
     lhs
     unfold denote denote.go
@@ -224,9 +220,9 @@ theorem denote_idx_gate {aig : AIG α} {hstart} (h : aig.decls[start] = .gate lh
     ⟦aig, ⟨start, hstart⟩, assign⟧
       =
     (
-      (xor ⟦aig, ⟨lhs, by have := aig.invariant hstart h; omega⟩, assign⟧ linv)
+      (⟦aig, ⟨lhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ linv)
         &&
-      (xor ⟦aig, ⟨rhs, by have := aig.invariant hstart h; omega⟩, assign⟧ rinv)
+      (⟦aig, ⟨rhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ rinv)
     ) := by
   unfold denote
   conv =>

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean

@@ -27,7 +27,7 @@ namespace blastAdd
 theorem denote_mkFullAdderOut (assign : α → Bool) (aig : AIG α) (input : FullAdderInput aig) :
     ⟦mkFullAdderOut aig input, assign⟧
       =
-    xor (xor ⟦aig, input.lhs, assign⟧ ⟦aig, input.rhs, assign⟧) ⟦aig, input.cin, assign⟧
+    ((⟦aig, input.lhs, assign⟧ ^^ ⟦aig, input.rhs, assign⟧) ^^ ⟦aig, input.cin, assign⟧)
     := by
   simp only [mkFullAdderOut, Ref.cast_eq, denote_mkXorCached, denote_projected_entry, Bool.bne_assoc,
     Bool.bne_left_inj]
@@ -37,10 +37,7 @@ theorem denote_mkFullAdderOut (assign : α → Bool) (aig : AIG α) (input : Ful
 theorem denote_mkFullAdderCarry (assign : α → Bool) (aig : AIG α) (input : FullAdderInput aig) :
     ⟦mkFullAdderCarry aig input, assign⟧
       =
-      ((xor
-          ⟦aig, input.lhs, assign⟧
-          ⟦aig, input.rhs, assign⟧) &&
-        ⟦aig, input.cin, assign⟧ ||
+      ((⟦aig, input.lhs, assign⟧ ^^ ⟦aig, input.rhs, assign⟧) && ⟦aig, input.cin, assign⟧ ||
        ⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧)
     := by
   simp only [mkFullAdderCarry, Ref.cast_eq, Int.reduceNeg, denote_mkOrCached,
@@ -133,7 +130,7 @@ theorem go_get (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig)
 theorem atLeastTwo_eq_halfAdder (lhsBit rhsBit carry : Bool) :
     Bool.atLeastTwo lhsBit rhsBit carry
       =
-    (((xor lhsBit rhsBit) && carry) || (lhsBit && rhsBit)) := by
+    (((lhsBit ^^ rhsBit) && carry) || (lhsBit && rhsBit)) := by
   revert lhsBit rhsBit carry
   decide
 

src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean

@@ -33,7 +33,7 @@ def toString : Gate → String
 def eval : Gate → Bool → Bool → Bool
   | and => (· && ·)
   | or => (· || ·)
-  | xor => Bool.xor
+  | xor => (· ^^ ·)
   | beq => (· == ·)
   | imp => (!· || ·)
 

src/Std/Tactic/BVDecide/Normalize/Bool.lean

@@ -46,7 +46,7 @@ attribute [bv_normalize] Bool.and_self_left
 attribute [bv_normalize] Bool.and_self_right
 
 @[bv_normalize]
-theorem Bool.not_xor : ∀ (a b : Bool), !(xor a b) = (a == b) := by decide
+theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b) := by decide
 
 end Normalize
 end Std.Tactic.BVDecide

src/Std/Tactic/BVDecide/Reflect.lean

@@ -126,7 +126,7 @@ theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
   simp[*]
 
 theorem xor_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
-    (Bool.xor lhs' rhs') = (xor lhs rhs) := by
+    (lhs' ^^ rhs') = (lhs ^^ rhs) := by
   simp[*]
 
 theorem beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :

tests/bench/bv_decide_realworld.lean

@@ -29,7 +29,7 @@ def parity32_spec_rec (i : Nat) (x : BitVec 32) : Bool :=
   | 0 => false
   | i' + 1 =>
     let bit_idx := BitVec.getLsbD x i'
-    Bool.xor bit_idx (parity32_spec_rec i' x)
+    bit_idx ^^ (parity32_spec_rec i' x)
 
 def parity32_spec (x : BitVec 32) : Bool :=
   parity32_spec_rec 32 x

tests/lean/run/bv_substructure.lean

@@ -14,7 +14,7 @@ theorem substructure_unit_1'' (x y z : BitVec 8) : (Bool.and (x = y) (y = z))
 theorem substructure_unit_2 (x y : BitVec 8) : x = y → y = x := by
   bv_decide
 
-theorem substructure_unit_3 (x y : BitVec 8) : xor (x = y) (y ≠ x) := by
+theorem substructure_unit_3 (x y : BitVec 8) : (x = y) ^^ (y ≠ x) := by
   bv_decide
 
 theorem substructure_unit_3' (x y : BitVec 8) : Bool.xor (x = y) (y ≠ x) := by

tests/lean/run/scopedParsers2.lean

@@ -16,15 +16,15 @@ namespace Foo
 
 def f x y := x + y + 1
 
-scoped infix:70 "^^" => f
+scoped infix:70 "~~" => f
 
-#check 1 ^^ 2
+#check 1 ~~ 2
 
-theorem ex1 : x ^^ y = f x y := rfl
+theorem ex1 : x ~~ y = f x y := rfl
 
 end Foo
 
-#check 1 ^^ 2 -- works because we have an `open Foo` above
+#check 1 ~~ 2 -- works because we have an `open Foo` above
 
-theorem ex2 : x ^^ y = f x y := rfl
-theorem ex3 : x ^^ y = Foo.f x y := rfl
+theorem ex2 : x ~~ y = f x y := rfl
+theorem ex3 : x ~~ y = Foo.f x y := rfl