		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::help

(macro) proof-builder help facility

Examples:

(help rewrite)   -- documentation on the proof-builder rewrite command
(help)           -- this help
(help help)      -- same as (help) or simply, help
(help all)       -- same as (doc proof-builder-commands)

General Forms:
(help) ; or, just: help
(help command)
(help all)

For any interactive proof-builder command, C, (help C) prints documentation on C to the terminal. You can read that documentation online or in the Emacs ACL2-Doc browser by viewing topic acl2-pc::C; see documentation.

To see a list of all interactive proof-builder commands, you can submit (help all). This is actually equivalent to (doc proof-builder-commands), which prints the documentation for topic proof-builder-commands (which, as discussed above, you can view online or with ACL2-Doc).

Also see ACL2-pc::doc, which provides a direct interface to the ACL2 :doc command. For example, submitting (help rewrite) to the interactive proof-builder is equivalent to submitting (doc acl2-pc::rewrite) to the proof-builder or submitting :doc acl2-pc::rewrite directly to the ACL2 loop.