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.
