reduce_interface : string * term -> unit
- SYNOPSIS
-
Remove a specific overload/interface mapping for an identifier.
- DESCRIPTION
-
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 CONDITIONS
-
Never fails, whether or not there were any interface mappings in effect.
- SEE ALSO
-
overload_interface, override_interface, remove_interface, the_interface.