(macro) proof-checker help facility


(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.)

To summarize: 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).