type_abbrev_pp
Parse.type_abbrev_pp : string * hol_type -> unit
Installs type abbreviation affecting parsing and printing.
As with type_abbrev(s,ty), a call to type_abbrev_pp(s,ty) sets up
the string s to be an abbrevation for the type ty when types are
parsed. In addition, it causes the type pretty-printer to prefer the
abbreviation when it comes to print types that match the implicit
pattern specified by ty (which may include type variables).
Failure
Fails if the provided type is a single type variable.
Example
> type_abbrev_pp ("foo", ``:num -> 'a # num``);
val it = () : unit
> ``:bool foo``;
val it = ``:bool foo``: hol_type
> dest_thy_type it;
val it = {Args = [``:num``, ``:bool # num``],
Thy = "min", Tyop = "fun"}:
{Args: hol_type list, Thy: string, Tyop: string}