Major Section: EVENTS
Examples: (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. 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-irrelevant-formals-ok flg)where
flg is either t, nil, or :warn.
