From: Enrico Tassi <enrico.tassi@inria.fr>
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