equal
deleted
inserted
replaced
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 primrec ins List.list |
15 primrec |
16 "ins f x [] = [x]" |
16 "ins f x [] = [x]" |
17 "ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))" |
17 "ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))" |
18 primrec insort List.list |
18 primrec |
19 "insort f [] = []" |
19 "insort f [] = []" |
20 "insort f (x#xs) = ins f x (insort f xs)" |
20 "insort f (x#xs) = ins f x (insort f xs)" |
21 end |
21 end |
22 |
22 |