equal
deleted
inserted
replaced
7 |
7 |
8 AList = List + |
8 AList = List + |
9 |
9 |
10 consts |
10 consts |
11 |
11 |
12 alist_rec :: "[('a*'b) list,'c,['a,'b,('a*'b) list,'c]=>'c]=>'c" |
12 alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c" |
13 assoc :: "['a,'b,('a*'b) list] => 'b" |
13 assoc :: "['a,'b,('a*'b) list] => 'b" |
14 |
14 |
15 rules |
15 rules |
16 |
16 |
17 alist_rec_def |
17 alist_rec_def "alist_rec(al,b,c) == list_rec(al, b, split(c))" |
18 "alist_rec(al,b,c) == list_rec(al,b,%p xs g.split(p,%x y.c(x,y,xs,g)))" |
|
19 |
18 |
20 assoc_def "assoc(v,d,al) == alist_rec(al,d,%x y xs g.if(v=x,y,g))" |
19 assoc_def "assoc(v,d,al) == alist_rec(al,d,%x y xs g.if(v=x,y,g))" |
21 |
20 |
22 end |
21 end |