Return prover key checkpoint clauses programmatically.
Recall the key checkpoints printed at the end of a failed proof
attempt. Some are labeled ``Key checkpoint at the top level''; let us call
these checkpoints ``top-level'', and denote others as ``not top-level''. When
the most recent proof attempt was one that failed,
Related tools. Note that each returned checkpoint is a clause, that
is, a list of terms, implicitly disjoined. For a similar utility that
instead returns each checkpoint as an untranslated term such as one
would see during a proof, see checkpoint-list-pretty. See also show-checkpoint-list for a related tool that displays checkpoints rather than
returning them, and see checkpoint-info-list for a tool similar to
Here are details to keep in mind.
We therefore abandon our previous work on this conjecture and reassign the name *1 to the original conjecture.In that case, the unique top-level checkpoint is