ETA_CONV : conv
STRUCTURE
Drule
SYNOPSIS
Performs a toplevel eta-conversion.
DESCRIPTION
ETA_CONV
maps an eta-redex
\x. (t x)
, where
x
does not occur free in
t
, to the theorem
|- (\x. (t x)) = t
.
FAILURE
Fails if the input term is not an eta-redex.
SEEALSO
RIGHT_ETA
,
eta_conv
HOL
Kananaskis-13