mk_abs : term * term -> term
STRUCTURE
Term
SYNOPSIS
Constructs an abstraction.
DESCRIPTION
mk_abs (v, t)
returns the lambda abstraction
\v. t
. All free occurrences of
v
in
t
thereby become bound.
FAILURE
Fails if
v
is not a variable.
SEEALSO
dest_abs
,
is_abs
,
list_mk_abs
,
mk_var
,
mk_const
,
mk_comb
HOL
Kananaskis-13