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

- CURRY_CONV (Term `(\(x,y). x + y) z`);
> val it = |- (\(x,y). x + y) z = (\x y. x + y) (FST z) (SND z) : thm

FAILURE
CURRY_CONV tm fails if tm is not an application of a paired abstraction.
SEEALSO
HOL  Trindemossen-1