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

See also

boolSyntax.strip_comb, Term.mk_comb