list_mk_abs
Term.list_mk_abs : term list * term -> term
Also exported as boolSyntax.list_mk_abs.
Performs a sequence of lambda binding operations.
An application list_mk_abs ([v1,...,vn], M) yields the term
\v1 ... vn. M. Free occurrences of v1,...,vn in M become bound in
the result.
Failure
Fails if some vi (1 <= i <= n) is not a variable.
Example
> list_mk_abs ([mk_var("v1",bool),mk_var("v2",bool),mk_var("v3",bool)],
Term `v1 /\ v2 /\ v3`);
val it = “λv1 v2 v3. v1 ∧ v2 ∧ v3”: term
Comments
In the current implementation, list_mk_abs is more efficient than
iteration of mk_abs for larger tasks.
See also
Term.mk_abs,
boolSyntax.list_mk_forall,
boolSyntax.list_mk_exists