equal
deleted
inserted
replaced
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 "alist_rec(al,b,c) == list_rec(al, b, split(c))" |
17 alist_rec_def "alist_rec(al,b,c) == list_rec(b, split(c), al)" |
18 |
18 |
19 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))" |
20 |
20 |
21 end |
21 end |