hide_constant : string -> unit
- SYNOPSIS
-
Stops the quotation parser from recognizing a constant.
- DESCRIPTION
-
A call hide_constant "c" where c is the name of a constant, will
prevent the quotation parser from parsing it as such; it will just be parsed as
a variable. The effect can be reversed by unhide_constant "c".
- FAILURE CONDITIONS
-
Fails if the given name is not a constant of the current theory, or if the
named constant is already hidden.
- COMMENTS
-
The hiding of a constant only affects the quotation parser; the constant is
still there in a theory, and may not be redefined.
- SEE ALSO
-
unhide_constant.