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.