tysubst : (hol_type * hol_type) list -> hol_type -> hol_type

DESCRIPTION
The call tysubst [ty1',ty1; ... ; tyn',tyn] ty will systematically traverse the type ty and replace the topmost instances of any tyi encountered with the corresponding tyi'. In the (usual) case where all the tyi are type variables, this is the same as type_subst, but also works when they are not.

FAILURE CONDITIONS
Never fails. If several tyi are the same, the first one in the list will be used to determine the substitution.

EXAMPLE
  # tysubst [`:num`,`:A`; `:bool`,`:B`] `:A->(B)list->A#B#C`;;
  val it : hol_type = `:num->(bool)list->num#bool#C`
  # tysubst [`:A`,`:(num)list`] `:num->(num)list->(num)list`;;
  val it : hol_type = `:num->A->A`

SEE ALSO
inst, type_subst.