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
(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
moreif you don't necessarily want all the rest of the help at once. (Then keep typing
moreif 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
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
rewrite. In such cases,
command is treated identically