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