mk_icomb
boolSyntax.mk_icomb : term * term -> term
Forms an application term, possibly instantiating the function.
A call to mk_icomb(f,x) checks to see if the term f, which must have
function type, can have any of its type variables instantiated so as to
make the domain of the function match the type of x. If so, then the
call returns the application of the instantiated f to x.
Failure
Fails if there is no way to instantiate the function term to make its domain match the argument's type.
Example
Note how both the S combinator and the argument have type variables invented for them when the two quotations are parsed.
- val t = mk_icomb(``S``, ``\n:num b. (n,b)``);
<<HOL message: inventing new type variable names: 'a, 'b, 'c>>
<<HOL message: inventing new type variable names: 'a>>
> val t = ``S (\n b. (n,b))`` : term
The resulting term t has only the type variable :'a left after
instantiation.
- type_of t;
> val it = ``:(num -> 'a) -> num -> num # 'a`` : hol_type
This term can now be combined with an argument and the final type variable instantiated:
- mk_icomb(t, ``ODD``);
> val it = ``S (\n b. (n,b)) ODD`` : term
- type_of it;
> val it = ``:num -> num # bool``;
Attempting to use mk_comb above results in immediate error because it
requires domain and arguments types to be identical:
- mk_comb(``S``, ``\n:num b. (n,b)``) handle e => Raise e;
<<HOL message: inventing new type variable names: 'a, 'b, 'c>>
<<HOL message: inventing new type variable names: 'a>>
Exception raised at Term.mk_comb:
incompatible types
! Uncaught exception:
! HOL_ERR