New function list_forall_default3. 3 euros to the first one that reuses this function

(not artificially)

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index 2f388c0b5e83bbad8ca5359f2d0d936d7aedeb38..0d19524dcf1842d2667f36de5286b7adfdfb8ba0 100644 (file)
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -155,6 +155,15 @@ let rec list_iter_default2 f l1 def l2 =
     | a::ta, [] -> f a def; list_iter_default2 f ta def [] 
 ;;
 
+let rec list_forall_default3 f l1 l2 def l3 = 
+  match l1,l2,l3 with
+    | [], [], _ -> true
+    | [], _, _
+    | _, [], _ -> raise (Invalid_argument "list_forall_default3")
+    | a::ta, b::tb, c::tc -> f a b c && list_forall_default3 f ta tb def tc
+    | a::ta, b::tb, [] -> f a b def && list_forall_default3 f ta tb def [] 
+;;
+
 let sharing_map f l =
   let unchanged = ref true in
   let rec aux b = function

diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli
index 22139c291da9cd18036f05c1ffc1b46a2d533489..1e2d8e04710ab55be1303d6c59b825bdceced20b 100644 (file)
--- a/helm/software/components/extlib/hExtlib.mli
+++ b/helm/software/components/extlib/hExtlib.mli
@@ -96,6 +96,10 @@ val sharing_map: ('a -> 'a) -> 'a list -> 'a list
    The second one can be shorter and is padded with a default value.
    This function cannot fail. *)
 val list_iter_default2: ('a -> 'b -> unit) -> 'a list -> 'b -> 'b list -> unit
+(* Checks a predicate in parallel on three lists, the first two having the same
+   length (otherwise it raises Invalid_argument). It stops when the first two
+   lists are empty. The third one can be shorter and is padded with a default value. *)
+val list_forall_default3: ('a -> 'b -> 'c -> bool) -> 'a list -> 'b list -> 'c -> 'c list -> bool
 
 
   (** split_nth n l