equal
deleted
inserted
replaced
10 val dest: ('a -> 'a * 'a) -> int -> 'a -> 'a list |
10 val dest: ('a -> 'a * 'a) -> int -> 'a -> 'a list |
11 val access: {left: 'a -> 'a, right: 'a -> 'a, init: 'a} -> int -> int -> 'a |
11 val access: {left: 'a -> 'a, right: 'a -> 'a, init: 'a} -> int -> int -> 'a |
12 val accesses: {left: 'a -> 'a, right: 'a -> 'a, init: 'a} -> int -> 'a list |
12 val accesses: {left: 'a -> 'a, right: 'a -> 'a, init: 'a} -> int -> 'a list |
13 end; |
13 end; |
14 |
14 |
15 structure BalancedTree: BALANCED_TREE = |
15 structure Balanced_Tree: BALANCED_TREE = |
16 struct |
16 struct |
17 |
17 |
18 fun make _ [] = raise Empty |
18 fun make _ [] = raise Empty |
19 | make _ [x] = x |
19 | make _ [x] = x |
20 | make f xs = |
20 | make f xs = |