UNCURRY_CONV

PairRules.UNCURRY_CONV : conv

Uncurrys an application of an abstraction.

Example

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

See also

PairRules.CURRY_CONV