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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
|
<html>
<head><title>DOCUMENTATION.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h1>DOCUMENTATION</h1>functions that display documentation at the terminal
<pre>Major Section: <a href="acl2-doc-major-topics.html">ACL2 Documentation</a>
</pre><p>
This section explains the ACL2 online documentation system. Thus,
it assumes that you are typing at the terminal, inside an ACL2
session. If you are reading this description in another setting
(for example, on paper), simply ignore the parts of this description
that involve typing at the terminal.<p>
For an introduction to the ACL2 online documentation system, type
<code>:</code><code><a href="MORE.html">more</a></code> below. Whenever the documentation system concludes with
``(type :more for more, :more! for the rest)'' you may type <code>:</code><code><a href="MORE.html">more</a></code>
to see the next block of documentation.<p>
Topics related to documentation are documented individually:
<p>
<ul>
<li><h3><a href="_star_TERMINAL-MARKUP-TABLE_star_.html">*TERMINAL-MARKUP-TABLE*</a> -- a <a href="MARKUP.html">markup</a> table used for printing to the terminal
</h3>
</li>
<li><h3><a href="ARGS.html">ARGS</a> -- <code>args</code>, <code><a href="GUARD.html">guard</a></code>, <code>type</code>, <code><a href="CONSTRAINT.html">constraint</a></code>, etc., of a function symbol
</h3>
</li>
<li><h3><a href="DOC.html">DOC</a> -- brief <a href="DOCUMENTATION.html">documentation</a> (type <code>:doc name</code>)
</h3>
</li>
<li><h3><a href="DOC_bang_.html">DOC!</a> -- all the <a href="DOCUMENTATION.html">documentation</a> for a name (type <code>:doc! name</code>)
</h3>
</li>
<li><h3><a href="DOC-STRING.html">DOC-STRING</a> -- formatted <a href="DOCUMENTATION.html">documentation</a> strings
</h3>
</li>
<li><h3><a href="DOCS.html">DOCS</a> -- available <a href="DOCUMENTATION.html">documentation</a> topics (by section)
</h3>
</li>
<li><h3><a href="HELP.html">HELP</a> -- brief survey of ACL2 features
</h3>
</li>
<li><h3><a href="MARKUP.html">MARKUP</a> -- the markup language for ACL2 <a href="DOCUMENTATION.html">documentation</a> strings
</h3>
</li>
<li><h3><a href="MORE.html">MORE</a> -- your response to <code>:</code><code><a href="DOC.html">doc</a></code> or <code>:</code><code><a href="MORE.html">more</a></code>'s ``<code>(type :more...)</code>''
</h3>
</li>
<li><h3><a href="MORE_bang_.html">MORE!</a> -- another response to ``(type :more for more, :more! for the rest)''
</h3>
</li>
<li><h3><a href="MORE-DOC.html">MORE-DOC</a> -- a continuation of the <code>:</code><code><a href="DOC.html">doc</a></code> <a href="DOCUMENTATION.html">documentation</a>
</h3>
</li>
<li><h3><a href="NQTHM-TO-ACL2.html">NQTHM-TO-ACL2</a> -- ACL2 analogues of Nqthm functions and commands
</h3>
</li>
</ul>
The ACL2 online documentation feature allows you to see extensive
documentation on many ACL2 functions and ideas. You may use the
documentation facilities to document your own ACL2 functions and
theorems.<p>
If there is some name you wish to know more about, then type
<pre>
ACL2 !>:doc name
</pre>
in the top-level loop. If the name is documented, a brief blurb
will be printed. If the name is not documented, but is ``similar''
to some documented names, they will be listed. Otherwise, <code>nil</code> is
returned.<p>
Every name that is documented contains a one-line description, a few
notes, and some details. <code>:</code><code><a href="DOC.html">Doc</a></code> will print the one-liner and the
notes. When <code>:</code><code><a href="DOC.html">doc</a></code> has finished it stops with the message
``(type :more for more, :more! for the rest)'' to remind you that details are
available. If you then type
<pre>
ACL2 !>:more
</pre>
a block of the continued text will be printed, again concluding
with ``(type :more for more, :more! for the rest)'' if the text continues
further, or concluding with ``<code>*-</code>'' if the text has been exhausted. By
continuing to type <code>:</code><code><a href="MORE.html">more</a></code> until exhausting the text you can read
successive blocks. Alternatively, you can type <code>:</code><code><a href="MORE_bang_.html">more!</a></code> to get all
the remaining blocks.<p>
If you want to get the details and don't want to see the elementary
stuff typed by <code>:</code><code><a href="DOC.html">doc</a></code> name, type:
<pre>
ACL2 !>:MORE-DOC name
</pre>
We have documented not just function names but names of certain
important ideas too. For example, see <a href="REWRITE.html">rewrite</a> and
see <a href="META.html">meta</a> to learn about <code>:</code><code><a href="REWRITE.html">rewrite</a></code> rules and <code>:</code><code><a href="META.html">meta</a></code> rules,
respectively. See <a href="HINTS.html">hints</a> to learn about the structure of the
<code>:</code><code><a href="HINTS.html">hints</a></code> argument to the prover. The <code><a href="DEFLABEL.html">deflabel</a></code> event
(see <a href="DEFLABEL.html">deflabel</a>) is a way to introduce a logical name for no
reason other than to attach documentation to it; also
see <a href="DEFDOC.html">defdoc</a>.<p>
How do you know what names are documented? There is a documentation
data base which is querried with the <code>:</code><code><a href="DOCS.html">docs</a></code> command.<p>
The documentation data base is divided into sections. The sections
are listed by
<pre>
ACL2 !>:docs *
</pre>
Each section has a name, <code>sect</code>, and by typing
<pre>
ACL2 !>:docs sect
</pre>
or equivalently
<pre>
ACL2 !>:doc sect
</pre>
you will get an enumeration of the topics within that section.
Those topics can be further explored by using <code>:</code><code><a href="DOC.html">doc</a></code> (and <code>:</code><code><a href="MORE.html">more</a></code>) on
them. In fact the section name itself is just a documented name.
<code>:</code><code><a href="MORE.html">more</a></code> generally gives an informal overview of the general subject of
the section.
<pre>
ACL2 !>:docs **
</pre>
will list all documented topics, by section. This fills several
pages but might be a good place to start.<p>
If you want documentation on some topic, but none of our names or
brief descriptions seem to deal with that topic, you can invoke a
command to search the text in the data base for a given string.
This is like the GNU Emacs ``<code><a href="APROPOS.html">apropos</a></code>'' command.
<pre>
ACL2 !>:docs "functional inst"
</pre>
will list every documented topic whose <code>:</code><code><a href="DOC.html">doc</a></code> or <code>:</code><code><a href="MORE-DOC.html">more-doc</a></code> text
includes the substring <code>"functional inst"</code>, where case and the exact
number of spaces are irrelevant.<p>
If you want documentation on an ACL2 function or macro and the
documentation data base does not contain any entries for it, there
are still several alternatives.
<pre>
ACL2 !>:args fn
</pre>
will print the arguments and some other relevant information about
the named function or macro. This information is all gleaned from
the definition (not from the documentation data base) and hence this
is a definitive way to determine if <code>fn</code> is defined as a function or
macro.<p>
You might also want to type:
<pre>
ACL2 !>:pc fn
</pre>
which will print the <a href="COMMAND.html">command</a> which introduced <code>fn</code>. You should
see <a href="COMMAND-DESCRIPTOR.html">command-descriptor</a> for details on the kinds of input you
can give the <code>:</code><code><a href="PC.html">pc</a></code> command.<p>
The entire ACL2 documentation data base is user extensible. That
is, if you document your function definitions or theorems, then that
documentation is made available via the data base and its query
commands.<p>
The implementation of our online documentation system makes use of
Common Lisp's ``documentation strings.'' While Common Lisp permits a
documentation string to be attached to any defined concept, Common
Lisp assigns no interpretation to these strings. ACL2 attaches
special significance to documentation strings that begin with the
characters ``<code>:doc-section</code>''. When such a documentation string is
seen, it is stored in the data base and may be displayed via <code>:</code><code><a href="DOC.html">doc</a></code>,
<code>:</code><code><a href="MORE.html">more</a></code>, <code>:</code><code><a href="DOCS.html">docs</a></code>, etc. Such documentation strings must follow rigid
syntactic rules to permit their processing by our commands. These
are spelled out elsewhere; see <a href="DOC-STRING.html">doc-string</a>.<p>
A description of the structure of the documentation data base may
also be found; see <a href="DOC-STRING.html">doc-string</a>.
<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>
|
