9 |
9 |
10 Term = CCL + |
10 Term = CCL + |
11 |
11 |
12 consts |
12 consts |
13 |
13 |
14 one :: "i" |
14 one :: "i" |
15 |
15 |
16 if :: "[i,i,i]=>i" ("(3if _/ then _/ else _)" [] 60) |
16 if :: "[i,i,i]=>i" ("(3if _/ then _/ else _)" [0,0,60] 60) |
17 |
17 |
18 inl,inr :: "i=>i" |
18 inl,inr :: "i=>i" |
19 when :: "[i,i=>i,i=>i]=>i" |
19 when :: "[i,i=>i,i=>i]=>i" |
20 |
20 |
21 split :: "[i,[i,i]=>i]=>i" |
21 split :: "[i,[i,i]=>i]=>i" |
22 fst,snd, |
22 fst,snd, |
23 thd :: "i=>i" |
23 thd :: "i=>i" |
24 |
24 |
25 zero :: "i" |
25 zero :: "i" |
26 succ :: "i=>i" |
26 succ :: "i=>i" |
27 ncase :: "[i,i,i=>i]=>i" |
27 ncase :: "[i,i,i=>i]=>i" |
28 nrec :: "[i,i,[i,i]=>i]=>i" |
28 nrec :: "[i,i,[i,i]=>i]=>i" |
29 |
29 |
30 nil :: "i" ("([])") |
30 nil :: "i" ("([])") |
31 "$" :: "[i,i]=>i" (infixr 80) |
31 "$" :: "[i,i]=>i" (infixr 80) |
32 lcase :: "[i,i,[i,i]=>i]=>i" |
32 lcase :: "[i,i,[i,i]=>i]=>i" |
33 lrec :: "[i,i,[i,i,i]=>i]=>i" |
33 lrec :: "[i,i,[i,i,i]=>i]=>i" |
34 |
34 |
35 let :: "[i,i=>i]=>i" |
35 let :: "[i,i=>i]=>i" |
36 letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" |
36 letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" |
37 letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" |
37 letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" |
38 letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" |
38 letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" |
39 |
39 |
40 "@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)" [] 60) |
40 "@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)" |
41 "@letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)" [] 60) |
41 [0,0,60] 60) |
42 "@letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" [] 60) |
|
43 "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" [] 60) |
|
44 |
42 |
45 napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)") |
43 "@letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)" |
|
44 [0,0,0,60] 60) |
|
45 |
|
46 "@letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" |
|
47 [0,0,0,0,60] 60) |
|
48 |
|
49 "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" |
|
50 [0,0,0,0,0,60] 60) |
|
51 |
|
52 napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) |
46 |
53 |
47 rules |
54 rules |
48 |
55 |
49 one_def "one == true" |
56 one_def "one == true" |
50 if_def "if b then t else u == case(b,t,u,% x y.bot,%v.bot)" |
57 if_def "if b then t else u == case(b,t,u,% x y.bot,%v.bot)" |