list_mk_comb : term * term list -> term

SYNOPSIS

Iteratively constructs combinations (function applications).

DESCRIPTION

list_mk_comb(`t`,[`t1`;...;`tn`]) returns `t t1 ... tn`.

FAILURE CONDITIONS

Fails with list_mk_comb 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(`1`,[]);;
  val it : term = `1`

  # list_mk_comb(`(/\)`,[`T`]);;
  val it : term = `(/\) T`

  # list_mk_comb(`(/\)`,[`1`]);;
  Exception: Failure "mk_comb: types do not agree".

SEE ALSO

list_mk_icomb, mk_comb, strip_comb.