ACL2-PC::HELP

(macro) proof-checker help facility 
Major Section:  PROOF-CHECKER-COMMANDS


Examples:

(help all)     -- list all proof-checker commands
(help rewrite) -- partial documentation on the rewrite command; the
                  rest is available using more or more!

(help! rewrite) -- full documentation on the rewrite command

help, help!     -- this documentation (in part, or in totality,
                   respectively)

General Forms:
(help &optional command)
(help! &optional command)
more
more!
The proof checker supports the same kind of documentation as does ACL2 proper. The main difference is that you need to type 
(help command)
in a list rather than :doc command. So, to get all the documentation on command, type (help! command) inside the interactive loop, but to get only a one-line description of the command together with some examples, type (help command). In the latter case, you can get the rest of the help by typing more!; or type more if you don't necessarily want all the rest of the help at once. (Then keep typing more if you want to keep getting more of the help for that command.)

An exception is (help all), which prints the documentation topic proof-checker-commands, to show you all possible proof-checker commands. So for example, when you see ACL2-PC::USE in that list, you can then submit (help use) or (help! use) to get documentation for the proof-checker use command.

But summarizing for other than the case of all: as with ACL2, you can type either of the following: 

more, more!
-- to obtain more (or, all the rest of) the documentation last
   requested by help (or, outside the proof-checker's loop, :doc)
It has been arranged that the use of (help command) will tell you just about everything you could want to know about command, almost always by way of examples. For more details about a command, use help!, more, or more!.

We use the word ``command'' to refer to the name itself, e.g. rewrite. We use the word ``instruction'' to refer to an input to the interactive system, e.g. (rewrite foo) or (help split). Of course, we allow commands with no arguments as instructions in many cases, e.g. rewrite. In such cases, command is treated identically to (command).