PETA_CONV : conv
STRUCTURE
PairRules
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-14