ACL2-pc::exit
(meta) exit the interactive proof-builder
Examples:
exit -- exit the interactive proof-builder
(exit t) -- exit after printing a bogus defthm event
(exit append-associativity) -- exit and create a defthm
event named append-associativity
General Forms:
exit -- Exit without storing an event.
(exit t) -- Exit after printing a bogus defthm event, showing :INSTRUCTIONS.
(exit event-name &optional rule-classes do-it-flg) --
Exit, and perhaps store an event
The command exit returns you to the ACL2 loop. At a later time,
(acl2::verify) may be executed to get back into the same interactive
proof-builder state, as long as there hasn't been an intervening use of the
proof-builder (otherwise see ACL2-pc::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 verify and ACL2-pc::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 ACL2-pc::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 neither (exit event-name ...) nor
(exit t) will cause an exit from the interactive loop. However, in
that case either one will print out the original user-supplied goal (the one
that was supplied with the call to verify) and the current list of
instructions.
