SET-IRRELEVANT-FORMALS-OK.html -- ACL2 Version 2.7

SET-IRRELEVANT-FORMALS-OK

allow irrelevant formals in definitions

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.

General Form:
(set-irrelevant-formals-ok flg)

where flg is either t, nil, or :warn.