mk_icomb : term * term -> term

SYNOPSIS

Makes a combination, instantiating types in rator if necessary.

DESCRIPTION

The call mk_icomb(f,x) makes the combination f x, just as with mk_comb, but if necessary to ensure the types are compatible it will instantiate type variables in f first.

FAILURE CONDITIONS

Fails if the rator type is impossible to instantiate compatibly.

EXAMPLE

The analogous call to the following using plain mk_const would fail:

  # mk_icomb(`(!)`,`\x. x = 1`);;
  Warning: inventing type variables
  val it : term = `!x. x = 1`

USES

A handy way of making combinations involving polymorphic constants, without needing a manual instantiation of the generic type.

SEE ALSO

list_mk_icomb, mk_comb, type_match.