16 list_rec :: "[i, i, [i,i,i]=>i] => i" |
16 list_rec :: "[i, i, [i,i,i]=>i] => i" |
17 map :: "[i=>i, i] => i" |
17 map :: "[i=>i, i] => i" |
18 length,rev :: "i=>i" |
18 length,rev :: "i=>i" |
19 flat :: "i=>i" |
19 flat :: "i=>i" |
20 list_add :: "i=>i" |
20 list_add :: "i=>i" |
|
21 hd,tl :: "i=>i" |
|
22 drop :: "[i,i]=>i" |
21 |
23 |
22 (* List Enumeration *) |
24 (* List Enumeration *) |
23 "[]" :: "i" ("[]") |
25 "[]" :: "i" ("[]") |
24 "@List" :: "args => i" ("[(_)]") |
26 "@List" :: "args => i" ("[(_)]") |
25 |
27 |
29 "[x]" == "Cons(x, [])" |
31 "[x]" == "Cons(x, [])" |
30 "[]" == "Nil" |
32 "[]" == "Nil" |
31 |
33 |
32 |
34 |
33 rules |
35 rules |
|
36 |
|
37 hd_def "hd(l) == list_case(0, %x xs.x, l)" |
|
38 tl_def "tl(l) == list_case(Nil, %x xs.xs, l)" |
|
39 drop_def "drop(i,l) == rec(i, l, %j r. tl(r))" |
|
40 |
34 list_rec_def |
41 list_rec_def |
35 "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))" |
42 "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))" |
36 |
43 |
37 map_def "map(f,l) == list_rec(l, Nil, %x xs r. Cons(f(x), r))" |
44 map_def "map(f,l) == list_rec(l, Nil, %x xs r. Cons(f(x), r))" |
38 length_def "length(l) == list_rec(l, 0, %x xs r. succ(r))" |
45 length_def "length(l) == list_rec(l, 0, %x xs r. succ(r))" |
39 app_def "xs@ys == list_rec(xs, ys, %x xs r. Cons(x,r))" |
46 app_def "xs@ys == list_rec(xs, ys, %x xs r. Cons(x,r))" |
40 rev_def "rev(l) == list_rec(l, Nil, %x xs r. r @ [x])" |
47 rev_def "rev(l) == list_rec(l, Nil, %x xs r. r @ [x])" |
41 flat_def "flat(ls) == list_rec(ls, Nil, %l ls r. l @ r)" |
48 flat_def "flat(ls) == list_rec(ls, Nil, %l ls r. l @ r)" |
42 list_add_def "list_add(l) == list_rec(l, 0, %x xs r. x#+r)" |
49 list_add_def "list_add(l) == list_rec(l, 0, %x xs r. x#+r)" |
43 |
|
44 end |
50 end |