UNPBETA_CONV : (term -> conv)
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Creates an application of a paired abstraction from a term.
DESCRIPTION
The user nominates some pair structure of variables
p
and a term
t
, and
UNPBETA_CONV
turns
t
into an abstraction on
p
applied to
p
.
------------------ UNPBETA_CONV "p" "t" |- t = (\p. t) p
FAILURE
Fails if
p
is not a paired structure of variables.
SEEALSO
PBETA_CONV
,
PAIRED_BETA_CONV
HOL
Kananaskis-13