12 ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list" |
12 ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list" |
13 insort :: "[['a,'a]=>bool, 'a list] => 'a list" |
13 insort :: "[['a,'a]=>bool, 'a list] => 'a list" |
14 |
14 |
15 rules |
15 rules |
16 ins_Nil "ins(f,x,[]) = [x]" |
16 ins_Nil "ins(f,x,[]) = [x]" |
17 ins_Cons "ins(f,x,Cons(y,ys)) = \ |
17 ins_Cons "ins(f,x,y#ys) = \ |
18 \ if(f(x,y), Cons(x,Cons(y,ys)), Cons(y, ins(f,x,ys)))" |
18 \ if(f(x,y), x#y#ys, y# ins(f,x,ys))" |
19 |
19 |
20 insort_Nil "insort(f,[]) = []" |
20 insort_Nil "insort(f,[]) = []" |
21 insort_Cons "insort(f,Cons(x,xs)) = ins(f,x,insort(f,xs))" |
21 insort_Cons "insort(f,x#xs) = ins(f,x,insort(f,xs))" |
22 end |
22 end |