From: Enrico Tassi Date: Wed, 30 Apr 2008 10:14:23 +0000 (+0000) Subject: added list_mapi X-Git-Tag: make_still_working~5280 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e48ac5af4e17dbac21b7e2767d4bd17f47ab19ea;p=helm.git added list_mapi --- diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index c2de58f81..fe587e297 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -140,6 +140,14 @@ let flatten_map f l = List.flatten (List.map f l) ;; +let list_mapi f l = + let rec aux k = function + | [] -> [] + | h::tl -> f h k :: aux (k+1) tl + in + aux 0 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 30a6f145f..5600bfbc7 100644 --- a/helm/software/components/extlib/hExtlib.mli +++ b/helm/software/components/extlib/hExtlib.mli @@ -90,6 +90,7 @@ 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 val list_last: 'a list -> 'a +val list_mapi: ('a -> int -> 'b) -> 'a list -> 'b list (** split_nth n l * @returns two list, the first contains at least n elements, the second the