An interactive tool for controlling ACL2's proof processes.

Call this up with

The *interactive proof-builder* provides a way to explore the
development of ACL2 proofs below the level of the ACL2 prover (as typically
used by `thm` and events such as `defthm`). To use this
tool, invoke the `verify` command, for example as follows.

ACL2 !>(verify (equal (append (append x y) z) (append x (append y z)))) ->:

Then at the `defthm` event if the goal stack is
empty; see proof-builder-commands, in particular the `instructions`
parameter, which directs replay of the interactive proof-builder commands (for
example during certification of a book containing that event; see books).

If you exit the interactive proof-builder's loop, you may re-enter that
session at the same point using the command

The interactive proof-builder can be invoked on a specific subgoal, and the
resulting

A tutorial is available here. That tutorial illustrates more than just the interactive proof-builder. The portion relevant to the proof-builder may be accessed directly here.

See set-evisc-tuple for how to arrange that output is printed in
abbreviated form. In general, the interactive proof-builder uses the

Individual proof-builder commands are documented in subsection proof-builder-commands. Note that the package name (see symbol-package-name is irrelevant for these commands (though not their
arguments); for example

The proof-builder supports user-defined macros, which are tactics that generate proof-builder instructions. See define-pc-macro.

*Remark.* The ``pc-'' prefix, for example in ``define-pc-macro''
above, stems from an earlier name for the proof-builder, which was
``proof-checker''. That also accounts for the string

- Instructions
- Instructions to the interactive proof-builder
- Proof-builder-commands
- List of commands for the interactive proof-builder
- Proof-builder-commands-short-list
- Perhaps the most commonly used proof-builder commands
- Dive-into-macros-table
- Right-associated function information for the proof-builder
- Verify
- Enter the interactive proof-builder
- Define-pc-macro
- Define a proof-builder macro command
- Macro-command
- Compound command for the interactive proof-builder
- Define-pc-help
- Define a macro command whose purpose is to print something
- Toggle-pc-macro
- Change an ordinary macro command to an atomic macro, or vice-versa
- Define-pc-meta
- Define a proof-builder meta command
- Retrieve
- Re-enter a (specified) proof-builder state
- Unsave
- Remove a proof-builder state
- Proof-checker
- Old name for proof-builder