list_mk_abs : term list * term -> term

SYNOPSIS

Iteratively constructs abstractions.

DESCRIPTION

list_mk_abs([`x1`;...;`xn`],`t`) returns `\x1 ... xn. t`.

FAILURE CONDITIONS

Fails with list_mk_abs if the terms in the list are not variables.

EXAMPLE

  # list_mk_abs([`m:num`; `n:num`],`m + n + 1`);;
  val it : term = `\m n. m + n + 1`

SEE ALSO

dest_abs, mk_abs, strip_abs.