A convenient marker for use with rebuild or ld
Example Input File for Rebuild:
(defun fn1 (x y) ...)
(defthm lemma1 ...)
(defthm lemma2 ...)
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
(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 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