mk_pabs : term * term -> term
STRUCTURE
pairSyntax
SYNOPSIS
Constructs a paired abstraction.
DESCRIPTION
If
M
is the tuple
(v1,..(..)..,vn)
, and
N
is an arbitrary term, then
mk_pabs (M,N)
returns the paired abstraction
`\(v1,..(..)..,vn).N`
.
FAILURE
Fails unless
M
is an arbitrarily nested pair composed from variables, with no repetitions of variables.
SEEALSO
dest_pabs
,
is_pabs
,
mk_abs
HOL
Kananaskis-14