Break-Rewrite Commands

Many commands display terms that are abbreviated (``eviscerated'')
by default. These have corresponding commands with a ``+'' suffix that avoid
such abbreviation, as shown below; also see brr-evisc-tuple. For
example, the notation ``

:a! abort to ACL2 top-level :ancestors[+] negations of backchaining hypotheses being pursued :btm[+] bottom-most frame in :path :eval try rule and re-enter break afterwards :eval! :eval but no recursive breaks :eval$ runes :eval with runes monitored during recursion :failure-reason[+] reason rule failed (after :eval) :final-ttree[+] ttree after :eval (see :DOC ttree) :frame[+] i ith frame in :path :go exit break, printing result :go! :go but no recursive breaks :go$ runes :go with runes monitored during recursion :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 [2], the right-hand side!) :ok exit break :ok! :ok but no recursive breaks :ok$ runes :ok with runes monitored during recursion :p! pop one level (exits a top-level break-rewrite loop) :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 [2], 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)

See the discussion of form [2] `rewrite-quoted-constant` rules
for an explanation of the swapped meanings of ``

Break-rewrite is just a call of the standard ACL2 read-eval-print
loop, `ld`, on a ``wormhole'' state. Thus, you may
execute most commands you might normally execute at the top-level of ACL2.
However, all state changes you cause from within break-rewrite
are lost when you exit or

Note that if you are breaking on a monitored linear rule,
several of the commands listed above do not apply: