The Theory combin

Parents

Children

Constants

$o	('b 'c) ('a 'b) 'a 'c
CombS	('a 'b 'c) ('a 'b) 'a 'c
CombK	'a 'b 'a
CombI	'a 'a

Fixity

Definitions

o
o_def	f g x (f o g) x = f (g x)
CombS
comb_s_def	f g x CombS f g x = f x (g x)
CombK
comb_k_def	x y CombK x y = x
CombI
comb_i_def	x CombI x = x

Theorems

s_k_thm	x CombS CombK x = CombI
o_assoc_thm	f g h f o g o h = (f o g) o h
o_i_thm	f CombI o f = f f o CombI = f

---

© created 1999/11/02 modified 1999/11/02