----------------------------------------------------------------------
type_subst                                                      (Type)
----------------------------------------------------------------------
type_subst : (hol_type,hol_type) subst -> hol_type -> hol_type

SYNOPSIS
Instantiates types in a type.

DESCRIBE
If {theta = [{redex_1,residue_1},...,{redex_n,residue_n}]} is a
{(hol_type,hol_type) subst}, where the {redex_i} are the types to
be substituted for, and the {residue_i} the replacements, and {ty}
is a type to instantiate, the call {type_subst theta ty}
will replace each occurrence of a {redex_i} by the
corresponding {residue_i} throughout {ty}. The replacements will be
performed in parallel. If several of the type instantiations are
applicable, the choice is undefined. Each {redex_i} ought to be a type
variable, but if it isn’t, it will never be replaced in {ty}. Also,
it is not necessary that any or all of the types {redex_1...redex_n}
should in fact appear in {ty}.

FAILURE
Never fails.

EXAMPLE

- type_subst [alpha |-> bool] (Type `:'a # 'b`);
> val it = `:bool # 'b` : hol_type

- type_subst [Type`:'a # 'b` |-> Type `:num`, alpha |-> bool]
             (Type`:'a # 'b`);
> val it = `:bool # 'b` : hol_type




SEEALSO
Term.inst, Thm.INST_TYPE, Lib.|->, Term.subst.

----------------------------------------------------------------------