allow irrelevant formals in definitions
Major Section:  EVENTS

(set-irrelevant-formals-ok t)
(set-irrelevant-formals-ok nil)
(set-irrelevant-formals-ok :warn)
The first example above allows irrelevant formals in definitions; see irrelevant-formals. The second example disallows irrelevant formals; this is the default. The third example allows irrelevant formals, 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.

General Form:
(set-irrelevant-formals-ok flg)
where flg is either t, nil, or :warn.