1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
\DOC remove_type_abbrev
\TYPE {remove_type_abbrev : string -> unit}
\SYNOPSIS
Removes use of name as a type abbreviation.
\DESCRIBE
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
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`)]
}
\noindent We can remove it again:
{
# remove_type_abbrev "btriple";;
val it : unit = ()
# type_abbrevs();;
val it : (string * hol_type) list = []
}
\SEEALSO
new_type_abbrev, type_abbrevs.
\ENDDOC
|
