boolSyntax.mk

Note how both the FOLDR combinator and the argument (the K combinator) have type variables invented for them when the two quotations are parsed.

   - val t = mk_ucomb(``FOLDR``, ``K``);
  <<HOL message: inventing new type variable names: 'a, 'b>>
  <<HOL message: inventing new type variable names: 'a, 'b>>
   > val t = ``FOLDR K`` : term

The resulting term t has only the type variable :'a left after instantiation.

   - type_of t;
   > val it = ``:'a -> 'a list -> 'a`` : hol_type

This term can now be combined with an argument and the final type variable instantiated:

   - mk_ucomb(t, ``T``);
   > val it = ``FOLDR K T`` : term

   - type_of it;
   > val it = ``:bool list -> bool``;

Attempting to use mk_icomb in the first example above results in immediate error because it can only instantiate the function type:

   - mk_icomb(``FOLDR``, ``K``) handle e => Raise e;
   <<HOL message: inventing new type variable names: 'a, 'b>>
   <<HOL message: inventing new type variable names: 'a, 'b>>

   Exception raised at HolKernel.list_mk_icomb:
   double bind on type variable 'b
   Exception-
      HOL_ERR
        {message = "double bind on type variable 'b", origin_function =
         "list_mk_icomb", origin_structure = "HolKernel"} raised

However it can be used in the second example, as only the function type requires instantiation:

   - mk_icomb(t, ``T``);
   > val it = ``FOLDR K T`` : term