boolSyntax.mk

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