Skip to content

Commit

Permalink
chore: use '^^' for Bool.* in ForLean (#657)
Browse files Browse the repository at this point in the history
  • Loading branch information
tobiasgrosser authored Sep 26, 2024
1 parent b24dc53 commit ac0a431
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions SSA/Projects/InstCombine/ForLean.lean
Original file line number Diff line number Diff line change
Expand Up @@ -631,24 +631,24 @@ theorem xor_decide (p q : Prop) [dp : Decidable p] [Decidable q] :
<;> simp [pt]

@[simp]
theorem xor_not_xor {a b : Bool} : xor (!xor a b) b = !a := by
theorem xor_not_xor {a b : Bool} : ((!(a ^^ b)) ^^ b) = !a := by
cases a
<;> cases b
<;> simp

@[simp]
theorem not_xor_and_self {a b : Bool} : (!xor a b && b) = (a && b) := by
theorem not_xor_and_self {a b : Bool} : (!(a ^^ b) && b) = (a && b) := by
cases a
<;> cases b
<;> simp

theorem xor_inv_left {a b c : Bool} : xor a b = c ↔ b = xor a c := by
theorem xor_inv_left {a b c : Bool} : (a ^^ b) = c ↔ b = (a ^^ c) := by
cases a
<;> cases b
<;> simp

@[simp]
theorem xor_ne_self {a b : Bool} : xor a ((!a) != b) = !b := by
theorem xor_ne_self {a b : Bool} : (a ^^ ((!a) != b)) = !b := by
cases a
<;> simp

Expand Down

0 comments on commit ac0a431

Please sign in to comment.