clear_overloads_on
Parse.clear_overloads_on : string -> unit
Clears all overloading on the specified operator.
This function removes all overloading associated with the given string,
except those "overloads" that map the string to constants of the same
name. These additional overloads (there may be more than one constant of
the same name, as long as each such is part of a different theory) may
be removed with remove_ovl_mapping, or by using hide.
Failure
Never fails. If a string is not overloaded, this function simply has no effect.
Example
> realTheory.REAL_INV_LT1;
val it =
⊢ ∀x. realax$real_lt (realax$real_of_num 0) x ∧
realax$real_lt x (realax$real_of_num 1) ⇒
realax$real_lt (realax$real_of_num 1) (realax$inv x): thm
> clear_overloads_on "<";
val it = (): unit
> realTheory.REAL_INV_LT1;
val it =
⊢ ∀x. realax$real_lt (realax$real_of_num 0) x ∧
realax$real_lt x (realax$real_of_num 1) ⇒
realax$real_lt (realax$real_of_num 1) (realax$inv x): thm
> clear_overloads_on "&";
val it = (): unit
> realTheory.REAL_INV_LT1;
val it =
⊢ ∀x. realax$real_lt (realax$real_of_num 0) x ∧
realax$real_lt x (realax$real_of_num 1) ⇒
realax$real_lt (realax$real_of_num 1) (realax$inv x): thm
If overloading gets too confusing, this function should help to clear away one layer of supposedly helpful obfuscation.
Comments
As with other parsing functions, there is a sister function,
temp_clear_overloads_on that does the same thing, but whose effect is
not saved to a theory file.