BRR-COMMANDS

Break-Rewrite Commands
Major Section:  BREAK-REWRITE

:a!             abort to ACL2 top-level
:p!             pop one level (exits a top-level break-rewrite loop)
:target         term being rewritten
:unify-subst    substitution making :lhs equal :target
:hyps           hypotheses of the rule
:hyp i          ith hypothesis of the rule
:lhs            left-hand side of rule's conclusion
:rhs            right-hand side of rule's conclusion
:type-alist     type assumptions governing :target
:initial-ttree  ttree before :eval (see ttree)
:ancestors      negations of backchaining hypotheses being pursued
:wonp           indicates if application succeed (after :eval)
:rewritten-rhs  rewritten :rhs (after :eval)
:final-ttree    ttree after :eval (see ttree)
:failure-reason reason rule failed (after :eval)
:path           rewrite's path from top clause to :target
:frame i        ith frame in :path
:top            top-most frame in :path
:ok             exit break
:go             exit break, printing result
:eval           try rule and re-enter break afterwards
:ok!            :ok but no recursive breaks
:go!            :go but no recursive breaks
:eval!          :eval but no recursive breaks
:ok$ runes      :ok with runes monitored during recursion
:go$ runes      :go with runes monitored during recursion
:eval$ runes    :eval with runes monitored during recursion
:help           this message
:standard-help  :help message from ACL2 top-level

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.