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

cond tt x y = x
cond ff x y = y

@[simp]

def bor :

bool → bool → bool

Boolean OR

Equations

tt || b = tt
ff || b = b

@[simp]

def band :

bool → bool → bool

Boolean AND

Equations

tt && b = b
ff && b = ff

@[simp]

def bnot :

Boolean NOT

Equations

!tt = ff
!ff = tt

@[simp]

def bxor :

bool → bool → bool

Boolean XOR

Equations