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 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
(i-am-here) need not be machine readable.