exit the interactive proof-checker
Major Section: PROOF-CHECKER-COMMANDS
Examples:
exit -- exit the interactive proof-checker
(exit append-associativity) -- exit and create a defthm
event named append-associativity
General Forms:
exit -- Exit without storing an event.
(exit event-name &optional rule-classes do-it-flg)
Exit, and store an event.
The command exit returns you to the ACL2 loop. At a later time,
(verify) may be executed to get back into the same proof-checker
state, as long as there hasn't been an intervening use of the
proof-checker (otherwise see save).When given one or more arguments as shown above, exit still returns
you to the ACL2 loop, but first, if the interactive proof is
complete, then it attempts create a defthm event with the specified
event-name and rule-classes (which defaults to (:rewrite) if not
supplied). The event will be printed to the terminal, and then
normally the user will be queried whether an event should really be
created. However, if the final optional argument do-it-flg is
supplied and not nil, then an event will be made without a query.
For example, the form
(exit top-pop-elim (:elim :rewrite) t)causes a
defthm event named top-pop-elim to be created with
rule-classes (:elim :rewrite), without a query to the user (because
of the argument t).Remark: it is permitted for event-name to be nil. In that case,
the name of the event will be the name supplied during the original call of
verify. (See the documentation for verify and commands.) Also
in that case, if rule-classes is not supplied then it defaults to the
rule-classes supplied in the original call of verify.
Comments on ``success'' and ``failure''. An exit instruction will
always ``fail'', so for example, if it appears as an argument of a
do-strict instruction then none of the later (instruction) arguments
will be executed. Moreover, the ``failure'' will be ``hard'' if an
event is successfully created or if the instruction is simply exit;
otherwise it will be ``soft''. See the documentation for sequence
for an explanation of hard and soft ``failures''. An obscure but
potentially important fact is that if the ``failure'' is hard, then
the error signal is a special signal that the top-level interactive
loop can interpret as a request to exit. Thus for example, a
sequencing command that turns an error triple (mv erp val state)
into (mv t val state) would never cause an exit from the interactive
loop.
If the proof is not complete, then (exit event-name ...) will not
cause an exit from the interactive loop. However, in that case it
will print out the original user-supplied goal (the one that was
supplied with the call to verify) and the current list of
instructions.
