mk_comb

Term.mk_comb : term * term -> term

Constructs a combination (function application).

mk_comb (t1,t2) returns the combination t1 t2.

Failure

Fails if t1 does not have a function type, or if t1 has a function type, but its domain does not equal the type of t2.

Example

   - mk_comb (neg_tm,T);

   > val it = `~T` : term

   - mk_comb(T, T) handle e => Raise e;

   Exception raised at Term.mk_comb:
   incompatible types

See also

Term.dest_comb, Term.is_comb, Term.list_mk_comb, Term.mk_var, Term.mk_const, Term.mk_abs