10 |
10 |
11 consts |
11 consts |
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 primrec ins List.list |
16 ins_Nil "ins(f,x,[]) = [x]" |
16 ins_Nil "ins(f,x,[]) = [x]" |
17 ins_Cons "ins(f,x,y#ys) = \ |
17 ins_Cons "ins(f,x,y#ys) = if(f(x,y), x#y#ys, y#ins(f,x,ys))" |
18 \ if(f(x,y), x#y#ys, y# ins(f,x,ys))" |
18 primrec insort List.list |
19 |
|
20 insort_Nil "insort(f,[]) = []" |
19 insort_Nil "insort(f,[]) = []" |
21 insort_Cons "insort(f,x#xs) = ins(f,x,insort(f,xs))" |
20 insort_Cons "insort(f,x#xs) = ins(f,x,insort(f,xs))" |
22 end |
21 end |