1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
<html>
<head><title>ACL2-PC_colon__colon_HELP.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>ACL2-PC::HELP</h3>(macro)
<code> </code>proof-checker help facility
<pre>Major Section: <a href="PROOF-CHECKER-COMMANDS.html">PROOF-CHECKER-COMMANDS</a>
</pre><p>
<pre>
Examples:<p>
(help rewrite) -- partial documentation on the rewrite command; the
rest is available using more or more!<p>
(help! rewrite) -- full documentation on the rewrite command<p>
help, help! -- this documentation (in part, or in totality,
respectively)
<p>
General Forms:
(help &optional command)
(help! &optional command)
more
more!
</pre>
The proof checker supports the same kind of documentation as does
ACL2 proper. The main difference is that you need to type
<pre>
(help command)
</pre>
in a list rather than <code>:doc command</code>. So, to get all the
documentation on <code>command</code>, type <code>(help! command)</code> inside the
interactive loop, but to get only a one-line description of the
command together with some examples, type <code>(help command)</code>. In the
latter case, you can get the rest of the help by typing <code>more!</code>; or
type <code>more</code> if you don't necessarily want all the rest of the help at
once. (Then keep typing <code>more</code> if you want to keep getting more of
the help for that command.)<p>
To summarize: as with ACL2, you can type either of the following:
<pre>
more, more!
-- to obtain more (or, all the rest of) the documentation last
requested by help (or, outside the proof-checker's loop, :doc)
</pre>
It has been arranged that the use of <code>(help command)</code> will tell you
just about everything you could want to know about <code>command</code>, almost
always by way of examples. For more details about a command, use
<code>help!</code>, <code>more</code>, or <code>more!</code>.<p>
We use the word ``command'' to refer to the name itself, e.g.
<code>rewrite</code>. We use the word ``instruction'' to refer to an input to
the interactive system, e.g. <code>(rewrite foo)</code> or <code>(help split)</code>. Of
course, we allow commands with no arguments as instructions in many
cases, e.g. <code>rewrite</code>. In such cases, <code>command</code> is treated identically
to <code>(command)</code>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
