mk_type : string * hol_type list -> hol_type
STRUCTURE
SYNOPSIS
Constructs a compound type.
DESCRIPTION
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 = `:'a -> 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.
SEEALSO
HOL  Kananaskis-14