----------------------------------------------------------------------
##                                                               (Lib)
----------------------------------------------------------------------
op ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd

SYNOPSIS
Infix combinator for applying two functions to the two projections of a pair.

DESCRIBE
An application {(f ## g) (x,y)} is equal to {(f x, g y)}.

FAILURE
If {f x} or {g y} fails.

EXAMPLE

- (I ## dest_imp) (strip_forall (Term `!x y z. x /\ y ==> z /\ p`));
> val it = ([`x`, `y`, `z`], (`x /\ y`, `z /\ p`))




COMMENTS
The {##} combinator can be thought of as a map operation for pairs.
It is declared as a right associative infix.

SEEALSO
Lib.pair.

----------------------------------------------------------------------