mk_select : term * term -> term
STRUCTURE
boolSyntax
SYNOPSIS
Constructs a choice-term.
DESCRIPTION
If
v
is a variable and
t
is a term of type
bool
, then
mk_select (v,t)
returns
@var. t
.
FAILURE
Fails if
v
is not a variable or if
t
is not of type
bool
.
SEEALSO
dest_select
,
is_select
HOL
Kananaskis-14