Major Section: EVENTS
Examples: (set-ignore-ok t) (set-ignore-ok nil) (set-ignore-ok :warn)The first example above allows unused formals and locals, i.e., variables that would normally have to be declared
ignorable. The second example disallows unused formals and locals; this is the default. The third example allows them, but prints an appropriate warning.
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
hence its effect is
local to the book or
containing it; see acl2-defaults-table.
General Form: (set-ignore-ok flg)where
One might find this event useful when one is generating function definitions by an automated procedure, when that procedure does not take care to make sure that all formals are actually used in the definitions that it generates.
Note: Defun will continue to report irrelevant formals even if
:set-ignore-ok has been set to
t, unless you also use
set-irrelevant-formals-ok to instruct it otherwise.