Checkpoint-list-pretty
Return prover key checkpoint goals programmatically.
See checkpoint-list for relevant background and related
utilities. Here we explain only how checkpoint-list-pretty differs from
checkpoint-list.
Recall that checkpoint-list returns a list of clauses or the keyword
:UNAVAILABLE. The corresponding value (checkpoint-list-pretty top-p
state) is obtained by replacing each such clause by a corresponding
untranslated term, which is the goal displayed during output from the
corresponding failed proof. For a clause with only one member, that is simply
the untranslation of that member. Otherwise the clause is a list (t0
... tn), in which case the corresponding untranslated term is an implication
(implies p q) , where p is formed by conjoining the untranslation
the negations of the ti for each i < n, and q is the
untranslation of tn.
Remarks.
- Untranslation is sensitive to let* abstraction; see set-let*-abstractionp.
- Unlike functions checkpoint-list and checkpoint-info-list, which
are guard-verified logic-mode functions,
checkpoint-list-pretty is a program-mode function.
- As with checkpoint-list, there is a special case when a proof attempt
is aborted in favor of proving the original goal by induction. With
checkpoint-list-pretty you will see (<GOAL>) to represent the list
of checkpoints as a list of terms: it shows that there is a single checkpoint
that is the original goal.
