A quick introduction to breaking rewrite rules in ACL2
Example: :brr t ; if you haven't done that yet :monitor (:rewrite lemma12) t ; to install a break point on the ; rule named (:rewrite lemma12) :monitor! (:rewrite lemma12) t ; quiet version of :monitor that ; invokes :brr t
ACL2 does not support Nqthm's
(1) To enable the ``break rewrite'' feature, you must first execute
ACL2 !>:brr t
at the top-level of ACL2. Equivalently, evaluate
(2) Decide what runes (see rune) you wish to monitor.
For example, you might want to know why
ACL2 !>:monitor (:rewrite lemma12 . 2) t
will install an ``unconditional'' break point on that rule. The ``
ACL2 !>(monitor '(:rewrite lemma12 . 2) t)
which you may also type. You may install breaks on as many rules as you wish. You must use monitor on each rule. You may also change the break condition on a rule with monitor. Use unmonitor (see unmonitor) to remove a rule from the list of monitored rules.
(3) Then try the proof again. When a monitored rule is tried by the
rewriter you will enter an interactive break, called break-rewrite.
See break-rewrite for a detailed description. Very simply, break-rewrite lets you inspect the context of the attempted application both
before and after the attempt. When break-rewrite is entered it will
print out the ``target'' term being rewritten. If you type
(4) When you have finished using the break-rewrite feature you should disable it to speed up the rewriter. You can disable it with
ACL2 !>:brr nil
The list of monitored rules and their break conditions persists but is ignored. If you enable break-rewrite later, the list of monitored rules will be displayed and will be used again by rewrite.
You should disable the break-rewrite feature whenever you are not intending to use it, even if the list of monitored rules is empty, because the rewriter is slowed down as long as break-rewrite is enabled.
If you get a stack overflow, see cw-gstack.