mathlib documentation

core / init.data.bool.basic

Boolean operations #

@[simp]
def cond {a : Type u} :
boola → a → a

cond b x y is x if b = tt and y otherwise.

Equations
@[simp]
def bor  :
boolboolbool

Boolean OR

Equations
@[simp]
def band  :
boolboolbool

Boolean AND

Equations
@[simp]
def bnot  :

Boolean NOT

Equations