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