Major Section: PROOF-CHECKER
The proof-checker (see proof-checker) allows the user to supply interactive commands. Compound commands, called macro commands, may be defined; these expand into zero or more other commands. Some of these are ``atomic'' macro commands; these are viewed as a single command step when completed successfully.
More documentation will be written on the proof-checker. For now,
we simply point out that there are lots of examples of the use of
define-pc-macro and define-pc-atomic-macro in the ACL2 source file
"proof-checker-b.lisp". The former is used to create macro
commands, which can be submitted to the interactive loop
(see verify) and will ``expand'' into zero or more commands.
The latter is similar, except that the undoing mechanism
(see acl2-pc::undo) understands atomic macro commands to
represent single interactive commands. Also see acl2-pc::comm
and see acl2-pc::commands for a discussion of the display of
interactive commands.
Also see toggle-pc-macro for how to change a macro command to
an atomic macro command, and vice versa.