Major Section: EVENTS
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. Moreover, its effect is to set the
acl2-defaults-table, and hence its effect is
localto the book or
encapsulateform containing it; see acl2-defaults-table.
General Form: (set-inhibit-warnings string1 string2 ...)where each string is considered without regard to case. This macro is equivalent to
(table acl2-defaults-table :inhibit-warnings lst), where
lstis the list of strings supplied. This macro is an event (see table), but no output results from a
The effect of this event is to suppress any warning whose label is a member of this list (where again, case is ignored). For example, the warning
ACL2 Warning [Use] in ( THM ...): It is unusual to :USE ....will not be printed if
"USE", etc.) is a member of the given list of strings.
Of course, if warnings are inhibited overall --
see set-inhibit-output-lst -- then the value of
:inhibit-warnings is entirely irrelevant.