mk_type
Type.mk_type : string * hol_type list -> hol_type
Constructs a compound type.
mk_type(tyop,[ty1,...,tyn]) returns the HOL type (ty1,...,tyn)tyop,
provided tyop is the name of a known n-ary type constructor.
Failure
Fails if tyop is not the name of a known type, or if tyop is known,
but the length of the list of argument types is not equal to the arity
of tyop.
Example
> mk_type ("bool",[]);
val it = “:bool”: hol_type
> mk_type ("fun",[alpha,it]);
val it = “:α -> bool”: hol_type
Comments
Note that type operators with the same name (and arity) may be declared
in different theories. If two theories having type operators with the
same name s are in the ancestry of the current theory, then
mk_type(s,tyl) will issue a warning before arbitrarily selecting which
type operator to use. In such situations, it is preferable to use
mk_thy_type since it allows one to specify exactly which type operator
to use.