From 4c18fa5b069a1e3216e9e3e0f18d92e778e67e41 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 10 Jul 2006 16:50:43 +0000 Subject: [PATCH] added flatten_map --- helm/software/components/extlib/hExtlib.ml | 4 ++++ helm/software/components/extlib/hExtlib.mli | 1 + 2 files changed, 5 insertions(+) diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index 57511db0e..b36a4d89d 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -135,6 +135,10 @@ let is_alphanum c = is_alpha c || is_digit c (** {2 List processing} *) +let flatten_map f l = + List.flatten (List.map f l) +;; + let rec list_uniq ?(eq=(=)) = function | [] -> [] | h::[] -> [h] diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli index 52b74429c..a38b09334 100644 --- a/helm/software/components/extlib/hExtlib.mli +++ b/helm/software/components/extlib/hExtlib.mli @@ -78,6 +78,7 @@ val list_uniq: val filter_map: ('a -> 'b option) -> 'a list -> 'b list (** filter + map *) val list_concat: ?sep:'a list -> 'a list list -> 'a list (**String.concat-like*) val list_findopt: ('a -> 'b option) -> 'a list -> 'b option +val flatten_map: ('a -> 'b list) -> 'a list -> 'b list (** {2 Debugging & Profiling} *) -- 2.39.2