1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
<html>
<head><title>BRR-COMMANDS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>BRR-COMMANDS</h2><a href="BREAK-REWRITE.html">Break-Rewrite</a> Commands
<pre>Major Section: <a href="BREAK-REWRITE.html">BREAK-REWRITE</a>
</pre><p>
<pre>
#. abort to ACL2 top-level
: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 <a href="TTREE.html">ttree</a>)
: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 <a href="TTREE.html">ttree</a>)
: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
</pre>
<p>
<a href="BREAK-REWRITE.html">Break-rewrite</a> is just a call of the standard ACL2 read-eval-print
loop, <code><a href="LD.html">ld</a></code>, on a ``<a href="WORMHOLE.html">wormhole</a>'' <a href="STATE.html">state</a>. Thus, you may execute most
commands you might normally execute at the top-level of ACL2.
However, all <a href="STATE.html">state</a> changes you cause from within <a href="BREAK-REWRITE.html">break-rewrite</a> are
lost when you exit or <code>:eval</code> the rule. You cannot modify <a href="STOBJ.html">stobj</a>s from
within the break. See <a href="BREAK-REWRITE.html">break-rewrite</a> for
more details and see <a href="LD.html">ld</a> for general information about the
standard ACL2 read-eval-print loop.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
