new_type_abbrev : string * hol_type -> unit
Sets up a new type abbreviation.
A call new_type_abbrev("ab",`:ty` creates a new type abbreviation ab for
the type ty. In future, `:ab` may be used rather than the perhaps
complicated expression `:ty`. Note that the association is purely an
abbreviation for parsing. Type abbreviations have no logical significance;
types are internally represented after the abbreviations have been fully
expanded. At present, type abbreviations are not reversed when printing types,
mainly because this may contract abbreviations where it is unwanted.
- FAILURE CONDITIONS
# new_type_abbrev("bitvector",`:bool list`);;
val it : unit = ()
val it : term = `LENGTH x`
# type_of (rand it);;
val it : hol_type = `:(bool)list`
- SEE ALSO
define_type, new_type_definition, remove_type_abbrev, type_abbrevs.