1\DOC
2
3\TYPE {mk_icomb : term * term -> term}
4
5\SYNOPSIS Forms an application term, possibly instantiating the function.
6
7\DESCRIBE
8A call to {mk_icomb(f,x)} checks to see if the term {f}, which must
9have function type, can have any of its type variables instantiated so
10as to make the domain of the function match the type of {x}.  If so,
11then the call returns the application of the instantiated {f} to {x}.
12
13\FAILURE
14Fails if there is no way to instantiate the function term to make its
15domain match the argument's type.
16
17\EXAMPLE
18
19Note how both the S combinator and the argument have type variables
20invented for them when the two quotations are parsed.
21{
22   - val t = mk_icomb(``S``, ``\n:num b. (n,b)``);
23  <<HOL message: inventing new type variable names: 'a, 'b, 'c>>
24  <<HOL message: inventing new type variable names: 'a>>
25   > val t = ``S (\n b. (n,b))`` : term
26}
27The resulting term {t} has only the type variable {:'a} left after
28instantiation.
29{
30   - type_of t;
31   > val it = ``:(num -> 'a) -> num -> num # 'a`` : hol_type
32}
33This term can now be combined with an argument and the final type
34variable instantiated:
35{
36   - mk_icomb(t, ``ODD``);
37   > val it = ``S (\n b. (n,b)) ODD`` : term
38
39   - type_of it;
40   > val it = ``:num -> num # bool``;
41}
42Attempting to use {mk_comb} above results in immediate error because
43it requires domain and arguments types to be identical:
44{
45   - mk_comb(``S``, ``\n:num b. (n,b)``) handle e => Raise e;
46   <<HOL message: inventing new type variable names: 'a, 'b, 'c>>
47   <<HOL message: inventing new type variable names: 'a>>
48
49   Exception raised at Term.mk_comb:
50   incompatible types
51   ! Uncaught exception:
52   ! HOL_ERR
53}
54
55\SEEALSO
56boolSyntax.list_mk_icomb, Term.mk_comb.
57
58\ENDDOC
59