mk_comb : term * term -> term
Constructs a combination.
Given two terms f and x, the call mk_comb(f,x) returns the combination or
application f x. It is necessary that f has a function type with domain
type the same as x's type.
- FAILURE CONDITIONS
Fails if the types of the terms are not compatible as specified above.
val it : term = `SUC 0`
Exception: Failure "mk_comb: types do not agree".
- SEE ALSO
dest_comb, is_comb, list_mk_comb, list_mk_icomb, mk_icomb.