diff options
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/util.mli b/lib/util.mli index ababb2ff9..e93094f89 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -123,6 +123,7 @@ val list_last : 'a list -> 'a val list_lastn : int -> 'a list -> 'a list val list_skipn : int -> 'a list -> 'a list val list_prefix_of : 'a list -> 'a list -> bool +val list_drop_prefix : 'a list -> 'a list -> 'a list (* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *) val list_map_append : ('a -> 'b list) -> 'a list -> 'b list (* raises [Invalid_argument] if the two lists don't have the same length *) |