mathlib documentation

core / init.data.bool.basic

Boolean operations #

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

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

Equations
@[simp]
def bor  :

Boolean OR

Equations
@[simp]
def band  :

Boolean AND

Equations
@[simp]
def bnot  :

Boolean NOT

Equations