]> matita.cs.unibo.it Git - helm.git/commitdiff
added list_mapi
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 30 Apr 2008 10:14:23 +0000 (10:14 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 30 Apr 2008 10:14:23 +0000 (10:14 +0000)
helm/software/components/extlib/hExtlib.ml
helm/software/components/extlib/hExtlib.mli

index c2de58f810fe99728b5b13253135c12934e02bec..fe587e297c50b5631d992852e12b2ae9bc84486c 100644 (file)
@@ -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]
index 30a6f145f11e22b0ad371d728182971d80cb5892..5600bfbc7e7c1c9b28c5f71480aad42180e2f2df 100644 (file)
@@ -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