rebuild
Major Section: MISCELLANEOUS
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.
(defthm lemma3 ...
:hints (("Goal" :use (:instance ???
...
By putting an (i-am-here) form at the ``frontier'' of an evolving file of
commands, you can use rebuild to load the file up to the
(i-am-here). I-am-here simply returns an error
triple (see error-triples) that indicates an error, and any form that
``causes an error'' will do the same job. Note that the text of the file
after the (i-am-here) need not be machine readable.
