mk_icomb : term * term -> term
Makes a combination, instantiating types in rator if necessary.
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.
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`
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.