UNCURRY_CONV : conv
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Uncurrys an application of an abstraction.
EXAMPLE
- UNCURRY_CONV (Term `(\x y. x + y) 1 2`);
> val it = |- (\x y. x + y) 1 2 = (\(x,y). x + y) (1,2) : thm

FAILURE
UNCURRY_CONV tm fails if tm is not double abstraction applied to two arguments
SEEALSO
CURRY_CONV
HOL  Trindemossen-1