Major Section: ACL2 Documentation
Call this up with
This is an interactive system for checking ACL2 theorems, or at least
exploring their proofs. One enters it using the
(see verify), and then invokes commands at the resulting prompt to operate
on a stack of goals, starting with the single goal that was supplied to
VERIFY. The final command (or ``instruction'') can be an
command, which can print out a
defthm event if the goal stack is empty;
see proof-checker-commands, in particular the
exit command. That
defthm event includes an
which directs replay of the proof-checker commands (for example during
certification of a book containing that event; see books).
If you exit the proof-checker interactive loop, you may re-enter that session
at the same point using the command
(verify), i.e., with no arguments.
retrieve may be invoked to manage more than one
The proof-checker can be invoked on a specific subgoal, and the resulting
:instructions can be given as a hint to the theorem prover for that
subgoal. See instructions.
A tutorial is available on the world-wide web:
The tutorial illustrates more than just the proof-checker. The portion relevant to the proof-checker may be accessed directly:
See set-evisc-tuple for how to arrange that output is printed in abbreviated
form. In general, the proof-checker uses the
described in that documentation.
Individual proof-checker commands are documented in subsection
proof-checker-commands. When inside the interactive loop (i.e., after
verify), you may use the
help command to get a list of
legal instructions and
(help instr) to get help for the instruction