I refer to the original feature request and comment on my modifications:
The command added to Abella is Reprove, since most of the top-level commands are capitalized.
Check that the last Top-level command was, in fact, Theorem. The reprove keyword should not be allowed immediately following a Definition, for example.
The check is done by a last_top_command variable introduced.
Check that the previous theorem has a completed proof.
The normal behavior of top-level commands is that one cannot invoke during the proof status. I don't check if the last proof was accepted, aborted, or partially skipped.
Reinstate the previous theorem and start reading the following text as a new proof of that theorem.
This is done by re-invoking the last Theorem command.
Example:
Theorem test_reprove : forall (a : o), a = a.
search.
Reprove.
intros. search.
Reprove.
intros. assert a = a. search.
This PR implements the feature requested by #133.
I refer to the original feature request and comment on my modifications:
The command added to Abella is
Reprove, since most of the top-level commands are capitalized.The check is done by a
last_top_commandvariable introduced.The normal behavior of top-level commands is that one cannot invoke during the proof status. I don't check if the last proof was accepted, aborted, or partially skipped.
This is done by re-invoking the last
Theoremcommand.Example: