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
mutual-recursion or
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 mutual-recursion or defuns
event. 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 acl2-defaults-table, and
hence its effect is local to the book or encapsulate form
containing it; see acl2-defaults-table.
General Form: (set-bogus-mutual-recursion-ok flg)where
flg is either t, nil, or :warn.
