Parse.type_abbrev

STRUCTURE

SYNOPSIS

Establishes a type abbreviation.

LIBRARY

Parse

DESCRIPTION

A call to type_abbrev(s,ty) sets up a type abbreviation that will cause the parser to treat the string s as a synonym for the type ty. Moreover, if ty includes any type variables, then the abbreviation is treated as a type operator taking as many parameters as appear in ty. The order of the parameters will be the alphabetic ordering of the type variables’ names.

Abbreviations work at the level of the names of type operators. It is thus possible to link a binary infix to an operator that is in turn an abbreviation.

FAILURE

Fails if the given type is just a type variable.

EXAMPLE

This is a simple abbreviation.

   > type_abbrev ("set", ``:'a -> bool``);
   val it = () : unit

   > ``:num set``;
   val it = ``:num -> bool`` : hol_type

Here, the abbreviation is set up and provided with its own infix symbol.

   - type_abbrev ("rfunc", ``:'b -> 'a``);
   > val it = () : unit

   - add_infix_type {Assoc = RIGHT, Name = "rfunc",
                     ParseName = SOME "<-", Prec = 50};
   > val it = () : unit

   - ``:'a <- bool``;
   > val it = ``:bool -> 'a`` : hol_type

   - dest_thy_type it;
   > val it = {Args = [``:bool``, ``:'a``], Thy = "min", Tyop = "fun"} :
      {Args : hol_type list, Thy : string, Tyop : string}

COMMENTS

As is common with most of the parsing and printing functions, there is a companion temp_type_abbrev function that does not cause the abbreviation effect to persist when the theory is exported. As the examples show, this entrypoint does not affect the pretty-printing of types. If printing of abbreviations is desired as well as parsing, the entrypoint type_abbrev_pp should be used.

SEEALSO

add_infix_type, disable_tyabbrev_printing, remove_type_abbrev, thytype_abbrev, type_abbrev_pp