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
|
<html>
<head><title>I-AM-HERE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>I-AM-HERE</h2>a convenient marker for use with <code><a href="REBUILD.html">rebuild</a></code>
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
<pre>
Example Input File for Rebuild:
(defun fn1 (x y) ...)
(defthm lemma1 ...)
(defthm lemma2 ...)
(i-am-here)
The following lemma won't go through. I started
typing the hint but realized I need to prove a
lemma first. See the failed proof attempt in foo.bar.
I'm going to quit for the night now and resume tomorrow
from home.<p>
(defthm lemma3 ...
:hints (("Goal" :use (:instance ???
...
</pre>
<p>
By putting an <code>(i-am-here)</code> form at the ``frontier'' of an evolving
file of <a href="COMMAND.html">command</a>s, you can use <code><a href="REBUILD.html">rebuild</a></code> to load the file up to the
<code>(i-am-here)</code>. <code>I-am-here</code> simply returns an <code><a href="LD.html">ld</a></code> error triple and any
form that ``causes an error'' will do the same job. Note that the
text of the file after the <code>(i-am-here)</code> need not be machine
readable.
<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>
|
