list_mk_icomb : term * term list -> term
STRUCTURE
SYNOPSIS
Folds mk_icomb over a series of arguments.
DESCRIPTION
A call to list_mk_icomb(f,args) combines f with each of the elements of the list args in turn, moving from left to right. If args is empty, then the result is simply f. When args is non-empty, the growing application-term is created with successive calls to mk_icomb, possibly causing type variables in any of the terms to become instantiated.
FAILURE
Fails if any of the underlying calls to mk_icomb fails, which will occur if the type of the accumulating term (starting with f) is not of a function type, or if it has a domain type that can not be instantiated to equal the type of the next argument term.
COMMENTS
list_mk_icomb is to mk_icomb what list_mk_comb is to mk_comb.
SEEALSO
HOL  Kananaskis-13