Structures · Data types
LawfulXor
A typeclass indicating that the xor operation, ^^^, is lawful.
- Defined in
- Mathlib.Data.LawfulXor.Basic
- Shape
- One type argument · adds xor_assoc, xor_self, xor_zero, xor_comm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances13
- Nat
- BitVec
- UInt64
- UInt8
- UInt16
- UInt32
- USize
- Int32
- Int8
- Int64
- Int16
- ISize
- Fin
How is a type an instance?
Loading the hierarchy index…
Assumed by32
- Equiv.xor
- LawfulXor.xor_comm
- zero_xor
- LawfulXor.xor_self
- LawfulXor.xor_zero
- xor_cancel_right
- LawfulXor.xor_assoc
- 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
Ancestors0
No ancestors.