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