Parse.disable_tyabbrev

STRUCTURE

SYNOPSIS

Disables the printing of a type abbreviation.

DESCRIPTION

A call to disable_tyabbrev_printing s causes the type abbreviation mapping the string s to some type expansion not to be printed when an instance of the type expansion is seen.

FAILURE

Never fails. If there is no abbreviation of the given name, a call to disable_tyabbrev_printing will silently do nothing.

EXAMPLE

- type_abbrev("LIST", ``:'a list``)
> val it = () : unit

- ``:num list``;
> val it = ``:num LIST`` : hol_type

- disable_tyabbrev_printing "LIST";
> val it = () : unit

- ``:num LIST``;
> val it = ``:num list`` : hol_type

COMMENTS

When a type-abbreviation is established with the function type_abbrev, this alters both parsing and printing: when the new abbreviation appears in input the type parser will translate away the abbreviation. Similarly, when an instance of the abbreviation appears in a type that the printer is to output, it will replace the instance with the abbreviation.

This is generally the appropriate behaviour. However, there is are a number of useful abbreviations where reversing parsing when printing is not so useful. For example, the abbreviation mapping 'a set to 'a -> bool is convenient, but it would be a mistake having it print because types such as that of conjunction would print as

   (/\) : bool -> bool set

which is rather confusing.

As with other printing and parsing functions, there is a version of this function, temp_disable_tyabbrev_printing that does not cause its effect to persist with an exported theory.

SEEALSO

type_abbrev