compound command for the proof-checker
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.