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
local to the book or encapsulate form in which it
occurs; see set-inhibit-warnings! for a corresponding non-local
event. Indeed, (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 lst is the list of strings supplied. This macro is an
event (see table), but no output results from a set-inhibit-warnings
event.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-warnings
is 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-warnings that contains the string, "Use" (or any string
that is string-equal to "Use", such as "use" or
"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
table named 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.
