basic_hol | |
sum | |
$o | ('b 'c) ('a 'b) 'a 'c |
CombS | ('a 'b 'c) ('a 'b) 'a 'c |
CombK | 'a 'b 'a |
CombI | 'a 'a |
Infix 300: | o |
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 |
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 |