CURRY_CONV

PairRules.CURRY_CONV : conv

Currys an application of a paired abstraction.

Example

> PairRules.CURRY_CONV (Term `(\(x,y). x + y) (1,2)`);
val it = ⊢ (λ(x,y). x + y) (1,2) = (λx y. x + y) 1 2: thm

> PairRules.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.

See also

PairRules.UNCURRY_CONV