Below is a list of commonly used break-rewrite keyword commands. These are only defined within the breaks caused by monitors on runes in the process of being considered by the ACL2 rewriter. These breaks interact with you from within a wormhole and are handled by ld (the same function that manages ACL2's top-level interactive read-eval-print loop). So within certain limitations imposed by wormholes, you can evaluate any command you would at the top-level of ACL2 in addition to the special commands below.
Many break commands display terms, e.g., the target being rewritten, and
“large” terms are “eviscerated” (i.e., abbreviated)
before printing. These commands have corresponding commands suffixed with a
``+'' that avoid evisceration so that the terms in question are printed in
full. See brr-evisc-tuple. The notation ``
:a! abort to ACL2 top-level :ancestors[+] negations of backchaining hypotheses being pursued :btm[+] bottom-most frame in :path :eval try the rule (i.e., recursively try to relieve the hypotheses and other conditions, possibly producing other breaks) and return to this break afterwards so you can query results :eval! :eval but remove all monitors first (see below) :eval$ runes :eval but first add monitors for runes (see below) :failure-reason[+] reason rule failed (after :eval) :final-ttree[+] ttree after :eval (see :DOC ttree) :frame[+] i ith frame in :path :go :eval but don't return to this break, just print the result of the try :go! :go but first remove all monitors (see below) :go$ runes :go but first add monitors for runes (see below) :help this message :hyp i ith hypothesis of the rule :hyps hypotheses of the rule :initial-ttree[+] ttree before :eval (see :DOC ttree) :lhs[+] left-hand side of rule's conclusion (or, in the case of :rewrite-quoted-constant rules of form , the right-hand side!); this is the pattern that the target must match for this :rewrite rule to fire :max-term[+] maximal term of a :linear lemma; this is the pattern that the target must match for this :linear rule to fire :ok like :go, but don't print the result of the try :ok! :ok but first remove all monitors (see below) :ok$ runes :ok but first add monitors for runes (see below) :path[+] rewriter's path from top clause to :target :poly-list[+] list of polynomials (after :eval) of a linear rule, where the leading term of each is enclosed in an extra set of parentheses :pot-list[+] set of polynomials governing :target, organized by maximal term :rewritten-rhs[+] rewritten :rhs (after :eval) of a rewrite rule :rhs right-hand side of rule's conclusion (or, in the case of :rewrite-quoted-constant rules of form , the left-hand side!) :standard-help :help message from ACL2 top-level :target[+] term being rewritten :top[+] top-most frame in :path :type-alist[+] type assumptions governing :target :unify-subst[+] substitution making :lhs equal :target :wonp indicates whether application succeeded (after :eval)
Since you're actually in a general read-eval-print loop when interacting
with break-rewrite you may type the usual ACL2 commands like
Note that if you are breaking on a monitored linear rule,
several of the commands listed above do not apply:
See the discussion of form 
This is useful if you want to monitor the use of a “secondary”
rune only during the attempt to apply a “primary” rune: install
the monitor on the secondary rune inside the break caused by the primary rune.
In the case of
Similar remarks apply to
Recall (from the discussion of monitors) that break conditions terms installed as part of break criteria do not just determine whether a break occurs but can compute the initial break commands fed to the interactive loop. Thus, for example, you can install a monitor that causes the rewriter to not only break when a certain rune is used, but then automatically print information, proceed from the break, inspect the result, and then either exit the break or prompt for user input. See the discussion in monitor.
Note: If you use commands that change the monitored runes during a break,
e.g., monitor, unmonitor, or