----------------------------------------------------------------------
PAIRED_ETA_CONV                                         (PairedLambda)
----------------------------------------------------------------------
PAIRED_ETA_CONV : conv

SYNOPSIS
Performs generalized eta conversion for tupled eta-redexes.

KEYWORDS
conversion, extensionality.

DESCRIBE
The conversion {PAIRED_ETA_CONV} generalizes {ETA_CONV} to eta-redexes with
tupled abstractions.

   PAIRED_ETA_CONV   \(v1..(..)..vn). f (v1..(..)..vn)
    = |- \(v1..(..)..vn). f (v1..(..)..vn) = f




FAILURE
Fails unless the given term is a paired eta-redex as illustrated above.

COMMENTS
Note that this result cannot be achieved by ordinary eta-reduction because
the tupled abstraction is a surface syntax for a term which does not
correspond to a normal pattern for eta reduction. Taking the term
apart reveals the true form of a paired eta redex:

   - dest_comb (Term `\(x:num,y:num). FST (x,y)`)
   > val it = (`UNCURRY`, `\x y. FST (x,y)`) : term * term




EXAMPLE
The following is a typical use of the conversion:

   val SELECT_PAIR_EQ = Q.prove
    (`(@(x:'a,y:'b). (a,b) = (x,y)) = (a,b)`,
     CONV_TAC (ONCE_DEPTH_CONV PairedLambda.PAIRED_ETA_CONV) THEN
     ACCEPT_TAC (SYM (MATCH_MP SELECT_AX (REFL (Term `(a:'a,b:'b)`)))));


SEEALSO
Drule.ETA_CONV.

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