mathlib documentation

lean_problem_sheets / 2020.logic.bool_not

source
inductive bool2  :
Type
source
@[protected, instance]
def bool2.fintype  :
fintype bool2
source
def bool2.and2  :
bool2 → bool2 → bool2
Equations
source
def bool2.or2  :
bool2 → bool2 → bool2
Equations
source
def bool2.not2  :
bool2 → bool2
Equations
source
def bool2.xor2 (x y : bool2) :
bool2
Equations
source
def bool2.going  :
bool2 → bool
Equations
source
def bool.to2  :
bool → bool2
Equations
source
def bool2.equiv  :
bool2 ≃ bool
Equations
source
def bimp  :
bool → bool → bool
Equations