diff options
Diffstat (limited to 'stdlib/list.mli')
| -rw-r--r-- | stdlib/list.mli | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/stdlib/list.mli b/stdlib/list.mli index 6484464a5..443d2317c 100644 --- a/stdlib/list.mli +++ b/stdlib/list.mli @@ -260,3 +260,17 @@ val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list The current implementation uses Merge Sort. It runs in constant heap space and logarithmic stack space. *) + +val fast_sort : ('a -> 'a -> int) -> 'a list -> 'a list +(** Same as {!List.sort} or {!List.stable_sort}, whichever is faster + on typical input. *) + +val merge : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list +(** Merge two lists: + Assuming that [l1] and [l2] are sorted according to the + comparison function [cmp], [merge cmp l1 l2] will return a + sorted list containting all the elements of [l1] and [l2]. + If several elements compare equal, the elements of [l1] will be + before the elements of [l2]. + Not tail-recursive (sum of the lenghts of the arguments). +*) |