SET-BOGUS-DEFUN-HINTS-OK.html -- ACL2 Version 6.2

SET-BOGUS-DEFUN-HINTS-OK

allow unnecessary ``mutual recursion''

Major Section:  SWITCHES-PARAMETERS-AND-MODES

General Forms:
(set-bogus-defun-hints-ok t)
(set-bogus-defun-hints-ok nil)
(set-bogus-defun-hints-ok :warn)

By default, ACL2 causes an error when the keyword :hints is supplied in an xargs declare form for a definition (see defun). This behavior can be defeated with (set-bogus-defun-hints-ok t), or if you still want to see a warning in such cases, (set-bogus-defun-hints-ok :warn).