Allow unused formals and locals without an
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
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-ignore-ok flg)
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