UNPBETA_CONV : (term -> conv)

- STRUCTURE
- 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

HOL Kananaskis-14