Structures · Lean core
XorOp
The homogeneous version of HXor: a ^^^ b : α where a b : α.
- Defined in
- Init.Prelude
- Shape
- One type argument · adds xor
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every XorOp is also a
Concrete types that are instances14
- Nat
- BitVec
- UInt64
- UInt8
- UInt16
- UInt32
- USize
- Int32
- Int8
- Int64
- Int16
- ISize
- Num
- Fin
How is a type an instance?
Loading the hierarchy index…
Assumed by28
- Equiv.xor
- zero_xor
- xor_cancel_right
- isFixedPt_xor_left_iff
- xor_right_involutive
- xor_left_eq_id_iff
- xor_right_eq
- xor_eq_iff_left_eq
- xor_right_eq_self_iff
- xor_eq_iff_right_eq
- xor_cancel_left
- xor_left_involutive
- Equiv.xor_involutive
- Equiv.isFixedPt_xor
- xor_left_eq_self_iff
- xor_xor_cancel_comm_assoc
- Equiv.xor_apply
- Equiv.xor_zero
- instAssociativeXor_mathlib
- isFixedPt_xor_right_iff
- xor_right_eq_id_iff
- Equiv.xor_eq_one_iff
- instLawfulCommIdentityXorOfNat_mathlib
- instCommutativeXor_mathlib
- xor_xor_cancel_comm
- xor_eq_zero_iff
- Equiv.xor_trans_xor
- Equiv.xor_symm