equal
deleted
inserted
replaced
8 *) |
8 *) |
9 |
9 |
10 ccc1 = Cprod3 + Sprod3 + Ssum3 + Lift3 + Fix + |
10 ccc1 = Cprod3 + Sprod3 + Ssum3 + Lift3 + Fix + |
11 |
11 |
12 consts |
12 consts |
|
13 ID :: "'a -> 'a" |
|
14 cfcomp :: "('b->'c)->('a->'b)->'a->'c" |
13 |
15 |
14 ID :: "'a -> 'a" |
16 syntax "@oo" :: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100) |
15 |
17 |
16 "@oo" :: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100) |
18 translations "f1 oo f2" == "cfcomp[f1][f2]" |
17 "cop @oo" :: "('b->'c)->('a->'b)->'a->'c" ("cfcomp") |
|
18 |
|
19 translations "f1 oo f2" => "cfcomp[f1][f2]" |
|
20 |
19 |
21 rules |
20 rules |
22 |
21 |
23 ID_def "ID ==(LAM x.x)" |
22 ID_def "ID ==(LAM x.x)" |
24 oo_def "cfcomp == (LAM f g x.f[g[x]])" |
23 oo_def "cfcomp == (LAM f g x.f[g[x]])" |