1\DOC all2
2
3\TYPE {all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool}
4
5\SYNOPSIS
6Tests whether a predicate holds pairwise throughout two lists.
7
8\DESCRIBE
9An invocation
10{
11   all2 P [x1,...,xn] [y1,...,yn]
12}
13equals
14{
15   P x1 y1 andalso .... andalso P xn yn
16}
17Also, {all2 P [] []} yields {true}.
18
19\FAILURE
20If {P x0,...,P x(j-1)} all evaluate to {true} and {P xj} raises an
21exception {e}, then
22{
23   all2 P [x0,...,x(j-1),xj,...,xn]
24}
25raises {e}.  An invocation {all2 P l1 l2} will also raise an exception
26if the length of {l1} is not equal to the length of {l2}.
27
28\EXAMPLE
29{
30- all2 equal [1,2,3] [1,2,3];
31> val it = true : bool
32
33- all2 equal [1,2,3] [1,2,3,4] handle e => Raise e;
34
35Exception raised at Lib.all2:
36different length lists
37! Uncaught exception:
38! HOL_ERR
39
40- all2 (fn _ => fn _ => raise Fail "") [] [];
41> val it = true : bool
42
43- all2 (fn _ => fn _ => raise Fail "") [1] [1];
44! Uncaught exception:
45! Fail  ""
46}
47
48
49\SEEALSO
50Lib.all.
51\ENDDOC
52