proof-checker help facility
Major Section: PROOF-CHECKER-COMMANDS
Examples:The proof checker supports the same kind of documentation as does ACL2 proper. The main difference is that you need to type(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!
(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).
