@[reducible, inline]
Boolean “exclusive or”. xor x y
can be written x ^^ y
.
x ^^ y
is true
when precisely one of x
or y
is true
. Unlike and
and or
, it does not
have short-circuiting behavior, because one argument's value never determines the final value. Also
unlike and
and or
, there is no commonly-used corresponding propositional connective.
Examples:
false ^^ false = false
true ^^ false = true
false ^^ true = true
true ^^ true = false
Conventions for notations in identifiers:
- The recommended spelling of
^^
in identifiers isxor
.
Equations
Instances For
Boolean “exclusive or”. xor x y
can be written x ^^ y
.
x ^^ y
is true
when precisely one of x
or y
is true
. Unlike and
and or
, it does not
have short-circuiting behavior, because one argument's value never determines the final value. Also
unlike and
and or
, there is no commonly-used corresponding propositional connective.
Examples:
false ^^ false = false
true ^^ false = true
false ^^ true = true
true ^^ true = false
Conventions for notations in identifiers:
- The recommended spelling of
^^
in identifiers isxor
.
Equations
Instances For
Equations
and #
or #
distributivity #
eq/beq/bne #
coercision related normal forms #
beq properties #
xor #
le/lt #
min/max #
injectivity lemmas #
toNat #
toInt #
ite #
forall #
exists #
cond #
@[reducible, inline, deprecated Bool.cond_then_self (since := "2025-04-04")]
Equations
Instances For
@[reducible, inline, deprecated Bool.cond_else_self (since := "2025-04-04")]