1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
\DOC reduce_interface
\TYPE {reduce_interface : string * term -> unit}
\SYNOPSIS
Remove a specific overload/interface mapping for an identifier.
\DESCRIBE
HOL Light allows an identifier to map to a specific constant (see
{override_interface}) or be overloaded to several depending on type (see
{overload_interface}). A call to {remove_interface "ident"} removes all such
mappings for the identifier {ident}.
\FAILURE
Never fails, whether or not there were any interface mappings in effect.
\SEEALSO
overload_interface, override_interface, remove_interface, the_interface.
\ENDDOC
|
