PETA_CONV : conv
STRUCTURE
LIBRARY
pair
SYNOPSIS
Performs a top-level paired eta-conversion.
DESCRIPTION
PETA_CONV maps an eta-redex \p. t p, where none of variables in the paired structure of variables p occurs free in t, to the theorem |- (\p. t p) = t.
FAILURE
Fails if the input term is not a paired eta-redex.
HOL  Kananaskis-10