1\DOC list_mk_abs
2
3\TYPE {list_mk_abs : term list * term -> term}
4
5\SYNOPSIS
6Performs a sequence of lambda binding operations.
7
8\KEYWORDS
9variable, binding, abstraction.
10
11\DESCRIBE
12An application {list_mk_abs ([v1,...,vn], M)} yields the term
13{\v1 ... vn. M}. Free occurrences of {v1,...,vn} in {M} become bound
14in the result.
15
16\FAILURE
17Fails if some {vi} (1 <= i <= n) is not a variable.
18
19\EXAMPLE
20{
21- list_mk_abs ([mk_var("v1",bool),mk_var("v2",bool),mk_var("v3",bool)],
22               Term `v1 /\ v2 /\ v3`);
23> val it = `\v1 v2 v3. v1 /\ v2 /\ v3` : term
24}
25
26
27\COMMENTS
28In the current implementation, {list_mk_abs} is more efficient than
29iteration of {mk_abs} for larger tasks.
30
31\SEEALSO
32Term.mk_abs, boolSyntax.list_mk_forall, boolSyntax.list_mk_exists.
33\ENDDOC
34