BRR

to enable or disable the breaking of rewrite rules 
Major Section:  BREAK-REWRITE


Example:
:brr t       ; enable
:brr nil     ; disable


General Form:
(brr flg)
where flg evaluates to t or nil. This function modifies state so that the attempted application of certain rewrite rules are ``broken.'' ``Brr'' stands for ``break-rewrite'' and can be thought of as a mode with two settings. The normal mode is ``disabled.''

When brr mode is ``enabled'' the ACL2 rewriter monitors the attempts to apply certain rules and advises the user of those attempts by entering an interactive wormhole break. From within this break the user can watch selected application attempts. See break-rewrite.

The rules monitored are selected by using the monitor and unmonitor commands. It is possible to break a rune ``conditionally'' in the sense that an interactive break will occur only if a specified predicate is true of the environment at the time of the attempted application. See monitor and see unmonitor.

Even if a non-empty set of rules has been selected, no breaks will occur unless brr mode is enabled. Thus, the first time in a session that you wish to monitor a rewrite rule, use :brr t to enable brr mode. Thereafter you may select runes to be monitored with monitor and unmonitor with the effect that whenever monitored rules are tried (and their break conditions are met) an interactive break will occur. Be advised that when brr mode is enabled the rewriter is somewhat slower than normal. Furthermore, that sluggishness persists even if no runes are monitored. You may regain normal performance -- regardless of what runes are monitored -- by disabling brr mode with :brr nil.

Why isn't brr mode disabled automatically when no runes are monitored? More generally, why does ACL2 have brr mode at all? Why not just test whether there are monitored runes? If you care about the answers, see why-brr.