: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. Moreover, its effect is to set the
acl2-defaults-table, and
hence its effect is local to the book or encapsulate form
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 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.