Major Section: SWITCHES-PARAMETERS-AND-MODES
Examples: (set-inhibit-warnings "theory" "use")Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. It is
localto the book or
encapsulateform in which it occurs; see set-inhibit-warnings! for a corresponding non-
(set-inhibit-warnings ...)is equivalent to
(local (set-inhibit-warnings! ...)).
General Form: (set-inhibit-warnings string1 string2 ...)where each string is considered without regard to case. This macro is equivalent to
(local (table inhibit-warnings-table nil 'lst :clear)), where
lstis the list of strings supplied. This macro is an event (see table), but no output results from a
ACL2 prints warnings that may, from time to time, seem excessive to experienced users. Each warning is ``labeled'' with a string identifying the type of warning. Consider for example
ACL2 Warning [Use] in ( THM ...): It is unusual to :USE ....Here, the label is "Use". The argument list for
set-inhibit-warningsis a list of such labels, each of which is a string. Any warning is suppressed if its label is a member of this list, where case is ignored, . Thus, for example, the warning above will not be printed after a call of
set-inhibit-warningsthat contains the string,
"Use"(or any string that is
"Use", such as
"USE"). In summary: the effect of this event is to suppress any warning whose label is a member of the given argument list, where case is ignored.
The list of currently inhibited warnings is the list of keys in the
inhibit-warnings-table. (The values in the table are
irrelevant.) One way to get that value is to get the result from evaluating
the following form:
(table-alist 'inhibit-warnings-table (w state)). Of
course, if warnings are inhibited overall -- see set-inhibit-output-lst
-- then this value is entirely irrelevant.