----------------------------------------------------------------------
list_mk_comb                                                    (Term)
----------------------------------------------------------------------
list_mk_comb : term * term list -> term

SYNOPSIS
Iteratively constructs combinations (function applications).

DESCRIBE
{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 raised at Term.list_mk_comb:
incompatible types




SEEALSO
boolSyntax.strip_comb, Term.mk_comb.

----------------------------------------------------------------------