and #
Equations
or #
Equations
distributivity #
eq/beq/bne #
Equations
Equations
Equations
coercision related normal forms #
theorem
Bool.beq_eq_decide_eq
{α : Type u_1}
[BEq α]
[LawfulBEq α]
[DecidableEq α]
(a : α)
(b : α)
:
beq properties #
xor #
le/lt #
min/max #
injectivity lemmas #
toNat #
@[reducible, inline, deprecated Bool.toNat_le]