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