mathlib3 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

cond bool.tt x y = x
cond bool.ff x y = y

@[simp]

def bor :

bool → bool → bool

Boolean OR

Equations

bool.tt || b = bool.tt
bool.ff || b = b

@[simp]

def band :

bool → bool → bool

Boolean AND

Equations

bool.tt && b = b
bool.ff && b = bool.ff

@[simp]

def bnot :

Boolean NOT

Equations

!bool.tt = bool.ff
!bool.ff = bool.tt

@[simp]

def bxor :

bool → bool → bool

Boolean XOR

Equations