:inhibit-warnings is entirely irrelevant.
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 lst is the list of strings supplied. This macro is an event
(see table), but no output results from a
set-inhibit-warnings event.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" (or "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.