equal
deleted
inserted
replaced
37 "[x, xs]" == "Cons(x, [xs])" |
37 "[x, xs]" == "Cons(x, [xs])" |
38 "[x]" == "Cons(x, [])" |
38 "[x]" == "Cons(x, [])" |
39 "[]" == "Nil" |
39 "[]" == "Nil" |
40 |
40 |
41 |
41 |
42 rules |
42 defs |
43 |
43 |
44 hd_def "hd(l) == list_case(0, %x xs.x, l)" |
44 hd_def "hd(l) == list_case(0, %x xs.x, l)" |
45 tl_def "tl(l) == list_case(Nil, %x xs.xs, l)" |
45 tl_def "tl(l) == list_case(Nil, %x xs.xs, l)" |
46 drop_def "drop(i,l) == rec(i, l, %j r. tl(r))" |
46 drop_def "drop(i,l) == rec(i, l, %j r. tl(r))" |
47 |
47 |