ETA_CONV
Drule.ETA_CONV : conv
Performs a toplevel eta-conversion.
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.
Press ← or → to navigate between chapters
Press S or / to search in the book
Press ? to show this help
Press Esc to hide this help