From e59c9aa09523759787f2c227a3a128fb5faccd99 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 30 Jan 2008 04:10:42 +0000
Subject: Add list_iter3

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10481 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml  | 8 ++++++++
 lib/util.mli | 1 +
 2 files changed, 9 insertions(+)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index 32ede2fb24..5e3f7fa6bf 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -262,6 +262,14 @@ let rec list_fold_right_and_left f l hd =
     | a::l -> let hd = aux (a::tl) l in f hd a tl
    in aux [] l
 
+let list_iter3 f l1 l2 l3 =
+  let rec iter = function
+    | ([], [], []) -> ()
+    | ((h1::t1), (h2::t2), (h3::t3)) -> f h1 h2 h3; iter (t1,t2,t3)
+    | (_, _, _) -> invalid_arg "map3"
+  in 
+  iter (l1,l2,l3)
+
 let list_iter_i f l = list_fold_left_i (fun i _ x -> f i x) 0 () l
 
 let list_for_all_i p = 
diff --git a/lib/util.mli b/lib/util.mli
index 8e3ec2cb40..ae1b906ce1 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -111,6 +111,7 @@ val list_index : 'a -> 'a list -> int
 val list_unique_index : 'a -> 'a list -> int 
 (* [list_index0] behaves as [list_index] except that it starts counting at 0 *)
 val list_index0 : 'a -> 'a list -> int
+val list_iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
 val list_iter_i :  (int -> 'a -> unit) -> 'a list -> unit
 val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_fold_right_and_left :
-- 
cgit v1.2.3