SET-BOGUS-MUTUAL-RECURSION-OK

allow unnecessary ``mutual recursion''
Major Section:  EVENTS

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.