Major Section: ACL2 Documentation

Call this up with `(verify ...)`

.

### DEFINE-PC-HELP -- define a macro command whose purpose is to print something

### DEFINE-PC-MACRO -- define a proof-checker macro command

### DEFINE-PC-META -- define a proof-checker meta command

### INSTRUCTIONS -- instructions to the proof checker

### MACRO-COMMAND -- compound command for the proof-checker

### PROOF-CHECKER-COMMANDS -- list of commands for the proof-checker

### RETRIEVE -- re-enter a (specified) proof-checker state

### TOGGLE-PC-MACRO -- change an ordinary macro command to an atomic macro, or vice-versa

### UNSAVE -- remove a proof-checker state

### VERIFY -- enter the interactive proof checker

This is an interactive system for checking ACL2 theorems, or at least
exploring their proofs. One enters it using the `VERIFY`

command
(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 `exit`

command, which can print out a `defthm`

event if the goal stack is empty;
see proof-checker-commands, in particular the `exit`

command. That
resulting `defthm`

event includes an `:`

`instructions`

parameter,
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.
The commands `save`

and `retrieve`

may be invoked to manage more than one
session.

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:

http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html.

The tutorial illustrates more than just the proof-checker. The portion
relevant to the proof-checker may be accessed directly:

http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#slide29

See set-evisc-tuple for how to arrange that output is printed in abbreviated
form. In general, the proof-checker uses the `:TERM`

evisc-tuple
described in that documentation.

Individual proof-checker commands are documented in subsection
proof-checker-commands. When inside the interactive loop (i.e., after
executing `verify`

), you may use the `help`

command to get a list of
legal instructions and `(help instr)`

to get help for the instruction
`instr`

.