mk_abs : term * term -> term
SYNOPSIS
Constructs an abstraction.
DESCRIPTION
If
v
is a variable and
t
any term, then
mk_abs(v,t)
produces the abstraction term
\v. t
. It is not necessary that
v
should occur free in
t
.
FAILURE CONDITIONS
Fails if
v
is not a variable. See
mk_gabs
for constructing generalized abstraction terms.
EXAMPLE
# mk_abs(`x:num`,`x + 1`);; val it : term = `\x. x + 1`
SEE ALSO
dest_abs
,
is_abs
,
mk_gabs
.