		Search-engine friendly clone of the ACL2 documentation.

Break-rewrite

Brr-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 ``:ancestors[+]'' below indicates that the :ancestors command may abbreviate terms but the :ancestors+ command does not.

: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 ``:lhs'' and ``:rhs.''

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 :eval the rule. You cannot modify stobjs from within the break. See break-rewrite for more details and see ld for general information about the standard ACL2 read-eval-print loop. Also see brr@ for a utility that can return a value for many of the keywords above, instead of merely printing to the screen.

Note that if you are breaking on a monitored linear rule, several of the commands listed above do not apply: :lhs, :rhs, :initial-ttree, and :final-ttree. Moreover, :rewritten-rhs also does not apply, but instead, :poly-list shows the result of applying the linear lemma as a list of polynomials, implicitly conjoined. The leading term of each polynomial is enclosed in an extra set of parentheses.