(meta) exit the interactive proof-checker

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).

Note: 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.