dest_pselect : term -> term * term
STRUCTURE
pairSyntax
LIBRARY
pair
SYNOPSIS
Breaks apart a paired choice-term into the selected pair and the body.
DESCRIPTION
dest_pselect
is a term destructor for paired choice terms. The application of
dest_select
to
@pair. t
returns
(pair,t)
.
FAILURE
Fails with
dest_pselect
if term is not a paired choice-term.
SEEALSO
dest_select
,
is_pselect
HOL
Kananaskis-14