mathlib documentation

core.init.data.bool.basic

@[simp]

def cond {a : Type u} (a_1 : bool) (a_2 a_3 : a) :

a

Equations

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

@[simp]

def bor (a a_1 : bool) :

Equations

tt || _x = tt
ff || tt = tt
ff || ff = ff

@[simp]

def band (a a_1 : bool) :

Equations

tt && tt = tt
tt && ff = ff
ff && _x = ff

@[simp]

def bnot (a : bool) :

Equations

!tt = ff
!ff = tt

@[simp]

def bxor (a a_1 : bool) :

Equations