1\DOC mk_type
2
3\TYPE {mk_type : string * hol_type list -> hol_type}
4
5\SYNOPSIS
6Constructs a compound type.
7
8\DESCRIBE
9{mk_type(tyop,[ty1,...,tyn])} returns the HOL type {(ty1,...,tyn)tyop},
10provided {tyop} is the name of a known {n}-ary type constructor.
11
12\FAILURE
13Fails if {tyop} is not the name of a known type, or if {tyop} is known,
14but the length of the list of argument types is not equal to the arity
15of {tyop}.
16
17\EXAMPLE
18{
19- mk_type ("bool",[]);
20> val it = `:bool` : hol_type
21
22- mk_type ("fun",[alpha,it]);
23> val it = `:'a -> bool` : hol_type
24}
25
26
27\COMMENTS
28Note that type operators with the same name (and arity) may
29be declared in different theories. If two theories having type
30operators with the same name {s} are in the ancestry of the current
31theory, then {mk_type(s,tyl)} will issue a warning before arbitrarily
32selecting which type operator to use. In such situations, it is
33preferable to use {mk_thy_type} since it allows one to specify
34exactly which type operator to use.
35
36\SEEALSO
37Type.mk_thy_type, Type.dest_type, Type.mk_vartype, Type.-->.
38\ENDDOC
39