Filter
Top Products
6.2. TERMS 59
#type_of ‘x:A‘;;
it : hol_type = ‘:A‘
#type_of ‘x = x‘;;
Warning: inventing type variables
it : hol_type = ‘:bool‘
By analogy with HOL types, the rest of the functions divide nicely into those
for creating HOL terms, those for breaking them apart, and those for testing their
structure.
mk_var :string * hol_type -> term creates a HOL variable with the chosen
name and type.
#mk_var("x",mk_vartype "A");;
it : term = ‘x‘
#type_of it;;
it : hol_type = ‘:A‘
#mk_var("p",‘:bool‘);;
it : term = ‘p‘
mk_const :string * (hol_type * hol_type) list -> term is the analogous
constructor for HOL constants, but it’s a bit more complicated to use. The second
argument indicates not the desired type, but rather a list of settings for the type
variables in order to attain that type. For example:
#mk_const("=",[]);;
it : term = ‘(=)‘
#type_of it;;
it : hol_type = ‘:A->(A->bool)‘
#mk_const("=",[‘:bool‘,‘:A‘]);;
it : term = ‘(=)‘
#type_of it;;
it : hol_type = ‘:bool->(bool->bool)‘
There is an alternative function mk_mconst :string * hol_type -> term which
works out the instantiations itself. However it is not part of the logical core, relying
as it does on higher-level functions to match up types. It will fail if the desired type
cannot be realized:
#mk_mconst("=",‘:bool->bool->bool‘);;
it : term = ‘(=)‘
#type_of it;;
it : hol_type = ‘:bool->(bool->bool)‘
#mk_mconst("=",‘:A->B->C‘);;
Uncaught exception: Failure "mk_const: generic type cannot be instantiated"
mk_comb : term * term -> term creates an application; it is given two terms,
one a function and one an argument, and tries to create the corresponding applica-
tion term, failing if the types don’t match up.
#mk_comb(‘P:A->bool‘,‘x:A‘);;
it : term = ‘P x‘
#mk_comb(‘P:A->bool‘,‘x:B‘);;
Uncaught exception: Failure "mk_comb: types do not agree"
mk_abs :term * term -> term creates an abstraction term, given a variable
to abstract over and the term to act as body. It fails if the first term argument isn’t
a variable.