Allow irrelevant formals in definitions
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)
For a way to permit irrelevant formals in a specific definition, see declare.