UP

The Theory combin

Parents

basic_hol

Children

sum

Constants

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

Fixity

Infix 300:o

Definitions

o
o_defturnstil forall f g xspot (f o g) x = f (g x)
CombS
comb_s_defturnstil forall f g xspot CombS f g x = f x (g x)
CombK
comb_k_defturnstil forall x yspot CombK x y = x
CombI
comb_i_defturnstil forall xspot CombI x = x

Theorems

s_k_thmturnstil forall xspot CombS CombK x = CombI
o_assoc_thm turnstil forall f g hspot f o g o h = (f o g) o h
o_i_thmturnstil forall fspot CombI o f = f and f o CombI = f


HOME net links © RBJ created 1999/11/02 modified 1999/11/02