mk_exists : term * term -> term
STRUCTURE
boolSyntax
SYNOPSIS
Term constructor for existential quantification.
DESCRIPTION
If
v
is a variable and
t
is a term of type
bool
, then
mk_exists (v,t)
returns the term
?v. t
.
FAILURE
Fails if
v
is not a variable or if
t
is not of type
bool
.
SEEALSO
dest_exists
,
is_exists
,
list_mk_exists
,
strip_exists
HOL
Kananaskis-13