diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 7 | ||||
| -rw-r--r-- | lib/util.mli | 1 |
2 files changed, 8 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml index 3b04e25742..b7aa1fc0ee 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -946,6 +946,13 @@ let array_for_all4 f v1 v2 v3 v4 = lv1 = Array.length v4 && allrec (pred lv1) +let array_for_all_i f i v = + let rec allrec i = function + | -1 -> true + | n -> (f i v.(n)) && (allrec (i-1) (n-1)) + in + allrec i ((Array.length v)-1) + let array_hd v = match Array.length v with | 0 -> failwith "array_hd" diff --git a/lib/util.mli b/lib/util.mli index dc6498b15c..49e1fb4bd9 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -196,6 +196,7 @@ 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_for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool val array_hd : 'a array -> 'a val array_tl : 'a array -> 'a array val array_last : 'a array -> 'a |