PROOF-CHECKER

support for low-level interaction

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 theorems in ACL2. One enters it using VERIFY; see verify. The result of an interactive session is a defthm event with an :instructions parameter supplied. Such an event can be replayed later in a new ACL2 session with the ``proof-checker'' loaded.

Individual proof-checker commands are documented in subsection proof-checker-commands.

PROOF-CHECKER

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