control warnings

(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.