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.