From b2cf3bc56ebd4511070ccfedd0f0895a695a6b23 Mon Sep 17 00:00:00 2001 From: barras Date: Fri, 5 Mar 2004 21:35:15 +0000 Subject: modif des fixpoints pour que si on donne une notation au produit, les pts fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/util.ml | 19 +++++++++++++++++++ lib/util.mli | 4 ++++ 2 files changed, 23 insertions(+) (limited to 'lib') diff --git a/lib/util.ml b/lib/util.ml index f57b9a6db..f2af9f6d4 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -401,6 +401,25 @@ let array_for_all2 f v1 v2 = let lv1 = Array.length v1 in lv1 = Array.length v2 && allrec (pred lv1) +let array_for_all3 f v1 v2 v3 = + let rec allrec = function + | -1 -> true + | n -> (f v1.(n) v2.(n) v3.(n)) && (allrec (n-1)) + in + let lv1 = Array.length v1 in + lv1 = Array.length v2 && lv1 = Array.length v3 && allrec (pred lv1) + +let array_for_all4 f v1 v2 v3 v4 = + let rec allrec = function + | -1 -> true + | n -> (f v1.(n) v2.(n) v3.(n) v4.(n)) && (allrec (n-1)) + in + let lv1 = Array.length v1 in + lv1 = Array.length v2 && + lv1 = Array.length v3 && + lv1 = Array.length v4 && + allrec (pred lv1) + let array_hd v = match Array.length v with | 0 -> failwith "array_hd" diff --git a/lib/util.mli b/lib/util.mli index e2e46f528..121b114a7 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -136,6 +136,10 @@ val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list val array_exists : ('a -> bool) -> 'a array -> bool val array_for_all : ('a -> bool) -> 'a array -> bool val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool +val array_for_all3 : ('a -> 'b -> 'c -> bool) -> + 'a array -> 'b array -> 'c array -> bool +val array_for_all4 : ('a -> 'b -> 'c -> 'd -> bool) -> + 'a array -> 'b array -> 'c array -> 'd array -> bool val array_hd : 'a array -> 'a val array_tl : 'a array -> 'a array val array_last : 'a array -> 'a -- cgit v1.2.3