list_mk_comb
Term.list_mk_comb : term * term list -> term
Iteratively constructs combinations (function applications).
list_mk_comb(t,[t1,...,tn]) returns t t1 ... tn.
Failure
Fails if the types of t1,...,tn are not equal to the argument types
of t. It is not necessary for all the arguments of t to be given. In
particular the list of terms t1,...,tn may be empty.
Example
> list_mk_comb(conditional,[T, mk_var("one",alpha), mk_var("two",alpha)]);
val it = “if T then one else two”: term
> list_mk_comb(universal,[]);
val it = “$!”: term
> try list_mk_comb(universal,[F]);
Exception- Type error in function application.
Function: try list_mk_comb :
(term -> (term * term list) option) list -> term -> term
Argument: (universal, [F]) : term * term list
Reason:
Can't unify (term -> (term * term list) option) list to
term * term list (Incompatible types)
Fail "Static Errors" raised