SET-IGNORE-OK

allow unused formals and locals without an ignore declaration 
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 ignored. 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 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)
where flg is either t, nil, or :warn.

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.