The Theory log
Parents

min
Children

init
Constants
T
BOOL
$
('a BOOL) BOOL
$
('a BOOL) BOOL
F
BOOL
$
BOOL BOOL
$
BOOL BOOL BOOL
$
BOOL BOOL BOOL
OneOne
('a 'b) BOOL
Onto
('a 'b) BOOL
TypeDefn
('b BOOL) ('a 'b) BOOL
Fixity




Binder: Infix 30: Infix 40: Prefix 50:
Terminators

Definitions
T
t_def
T ( x x) = ( x x)
_def
$ = ( P P = ( x T))
_def
$ = ( P P ($ P))
F
f_def
F ( b b)
_def
$ = ( b b F)
_def
$ = ( b1 b2 b (b1 b2 b) b)
_def
$ = ( b1 b2 b (b1 b) (b2 b) b)
OneOne
one_one_def
OneOne = ( f x1 x2 f x1 = f x2 x1 = x2)
Onto
onto_def
Onto = ( f y x y = f x)
TypeDefn
type_defn_def
TypeDefn
= ( P rep
OneOne rep ( x P x ( y x = rep y)))

up quick index © RBJ