remove_type_abbrev : string -> unit

SYNOPSIS

Removes use of name as a type abbreviation.

DESCRIPTION

A call remove_type_abbrev "s" removes any use of s as a type abbreviation, whether there is one already. Note that since type abbreviations have no logical status, being only a parsing abbreviation, this has no logical significance.

FAILURE CONDITIONS

Never fails.

EXAMPLE

Suppose we set up a type abbreviation:

  # new_type_abbrev("btriple",`:bool#bool#bool`);;
  val it : unit = ()
  # type_abbrevs();;
  val it : (string * hol_type) list = [("btriple", `:bool#bool#bool`)]

We can remove it again:

  # remove_type_abbrev "btriple";;
  val it : unit = ()
  # type_abbrevs();;
  val it : (string * hol_type) list = []

SEE ALSO

new_type_abbrev, type_abbrevs.