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