mk_thy_type
Type.mk_thy_type
: {Thy:string, Tyop:string, Args:hol_type list} -> hol_type
Constructs a type.
If s is a string that has been previously declared to be a type with
arity type n in theory thy, and the length of tyl is equal to n,
then mk_thy_type{Tyop=s, Thy=thy, Args=tyl} returns the requested
compound type.
Failure
Fails if s is not the name of a type in theory thy, if thy is not
in the ancestry of the current theory, or if n is not the length of
tyl.
Example
> mk_thy_type {Tyop="fun", Thy="min", Args = [alpha,bool]};
val it = “:α -> bool”: hol_type
> try mk_thy_type {Tyop="bar", Thy="foo", Args = []};
Exception- HOL_ERR
(at Type.mk_thy_type:
the type operator "bar" has not been declared in theory "foo".) raised
Comments
In general, mk_thy_type is to be preferred over mk_type because HOL
provides a fresh namespace for each theory (mk_type is a holdover from
a time when there was only one namespace shared by all theories).
See also
Type.mk_type,
Type.dest_thy_type,
Term.mk_const,
Term.mk_thy_const