1\DOC type_abbrev
2
3\TYPE {Parse.type_abbrev : string * hol_type -> unit}
4
5\SYNOPSIS
6Establishes a type abbreviation.
7
8\KEYWORDS
9Parsing, HOL types.
10
11\LIBRARY
12Parse
13
14\DESCRIBE
15A call to {type_abbrev(s,ty)} sets up a type abbreviation that will
16cause the parser to treat the string {s} as a synonym for the type
17{ty}. Moreover, if {ty} includes any type variables, then the
18abbreviation is treated as a type operator taking as many parameters
19as appear in {ty}.  The order of the parameters will be the alphabetic
20ordering of the type variables' names.
21
22Abbreviations work at the level of the names of type operators.  It is
23thus possible to link a binary infix to an operator that is in turn an
24abbreviation.
25
26\FAILURE
27Fails if the given type is just a type variable.
28
29\EXAMPLE
30This is a simple abbreviation.
31{
32   > type_abbrev ("set", ``:'a -> bool``);
33   val it = () : unit
34
35   > ``:num set``;
36   val it = ``:num -> bool`` : hol_type
37}
38Here, the abbreviation is set up and provided with its own infix
39symbol.
40{
41   - type_abbrev ("rfunc", ``:'b -> 'a``);
42   > val it = () : unit
43
44   - add_infix_type {Assoc = RIGHT, Name = "rfunc",
45                     ParseName = SOME "<-", Prec = 50};
46   > val it = () : unit
47
48   - ``:'a <- bool``;
49   > val it = ``:bool -> 'a`` : hol_type
50
51   - dest_thy_type it;
52   > val it = {Args = [``:bool``, ``:'a``], Thy = "min", Tyop = "fun"} :
53      {Args : hol_type list, Thy : string, Tyop : string}
54}
55
56
57\COMMENTS
58As is common with most of the parsing and printing functions, there is
59a companion {temp_type_abbrev} function that does not cause the
60abbreviation effect to persist when the theory is exported.  As the
61examples show, this entrypoint does not affect the pretty-printing of
62types.  If printing of abbreviations is desired as well as parsing, the  entrypoint {type_abbrev_pp} should be used.
63
64\SEEALSO
65Parse.add_infix_type, Parse.disable_tyabbrev_printing, Parse.remove_type_abbrev, Parse.thytype_abbrev, Parse.type_abbrev_pp.
66\ENDDOC
67