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.