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