diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 3 | ||||
| -rw-r--r-- | lib/util.mli | 1 |
2 files changed, 4 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml index 2bbdc76cf9..a87b9f5107 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -457,6 +457,9 @@ let list_map4 f l1 l2 l3 l4 = in map (l1,l2,l3,l4) +let list_map_to_array f l = + Array.of_list (List.map f l) + let rec list_smartfilter f l = match l with [] -> l | h::tl -> diff --git a/lib/util.mli b/lib/util.mli index 8f8475afd7..380f58eaba 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -101,6 +101,7 @@ val list_map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list val list_map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list +val list_map_to_array : ('a -> 'b) -> 'a list -> 'b array val list_filter_i : (int -> 'a -> bool) -> 'a list -> 'a list |