Major Section: SWITCHES-PARAMETERS-AND-MODES
Examples: (set-bogus-mutual-recursion-ok t) (set-bogus-mutual-recursion-ok nil) (set-bogus-mutual-recursion-ok :warn)By default, ACL2 checks that when a ``clique'' of more than one function is defined simultaneously (using
defuns), then every body calls at least one of the functions in the ``clique.'' Below, we refer to definitional events that fail this check as ``bogus'' mutual recursions. The check is important because ACL2 does not store induction schemes for functions defined with other functions in a
defunsevent. Thus, ACL2 may have difficulty proving theorems by induction that involve such functions. Moreover, the check can call attention to bugs, since users generally intend that their mutual recursions are not bogus.
Nevertheless, there are times when it is advantageous to allow bogus mutual recursions, for example when they are generated mechanically, even at the expense of losing stored induction schemes. The first example above allows bogus mutual recursion. The second example disallows bogus mutual recursion; this is the default. The third example allows bogus mutual recursion, 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
hence its effect is
local to the book or
containing it; see acl2-defaults-table.
General Form: (set-bogus-mutual-recursion-ok flg)where