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>DOC.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>DOC</h2>brief <a href="DOCUMENTATION.html">documentation</a> (type <code>:doc name</code>)
<pre>Major Section: <a href="DOCUMENTATION.html">DOCUMENTATION</a>
</pre><p>
NOTE: The <code>:doc</code> command only makes sense at the terminal.
Furthermore it only works at the terminal when a ``full-size'' image
has been built. Most users will probably access the ACL2
documentation in other ways, as explained in the file <code>"doc/README"</code>
that comes with the ACL2 distribution.
<pre>
Examples:
ACL2 !>:doc DEFTHM ; print documentation of DEFTHM
ACL2 !>:doc logical-name ; print documentation of LOGICAL-NAME
ACL2 !>:doc "MY-PKG" ; print documentation of "MY-PKG"<p>
Related Topics:
:more ; continues last :doc or :more-doc text
:more-doc name ; prints more documentation for name
:docs ** ; lists all documented symbols
:docs "compil" ; documented symbols apropos "compil"
:DOC documentation ; describes how documentation works
<p>
General Form:
ACL2>:doc logical-name
</pre>
where <code><a href="LOGICAL-NAME.html">logical-name</a></code> is a logical name (see <a href="LOGICAL-NAME.html">logical-name</a>) for
which you hope there is <a href="DOCUMENTATION.html">documentation</a>. Chances are there is no
<a href="DOCUMENTATION.html">documentation</a> at the moment, but we are working on adding
<a href="DOCUMENTATION.html">documentation</a> strings for all the user level ACL2 functions.<p>
For a general discussion of our treatment of documentation strings,
see <a href="DOCUMENTATION.html">documentation</a>.<p>
This is the first cut at online <a href="DOCUMENTATION.html">documentation</a>. Users can be
particularly helpful by sending mail on the inadequacies of the
system. Address it just to Moore and put <a href="DOCUMENTATION.html">Documentation</a> in the
subject line. There are several things that trouble me about what
I've done here.<p>
First, many concepts aren't documented. Ultimately, I'd like to
. document (a) every CLTL primitive (e.g., <code><a href="CASE.html">case</a></code> and <code><a href="COERCE.html">coerce</a></code>) and (b)
every ACL2 extension (e.g., <code><a href="AREF1.html">aref1</a></code> and <code>getprop</code>). But so far I have
focussed on documenting (c) the ACL2 system primitives (e.g., <code><a href="DEFTHM.html">defthm</a></code>
and what <code><a href="HINTS.html">hints</a></code> look like). My priorities are (c), then (b), and
then (a), following the philosophy that the most unstable features
should get online <a href="DOCUMENTATION.html">documentation</a> in these early releases. Having
gotten the basic <a href="DOCUMENTATION.html">documentation</a> in place, I'll document new things as
they are added, and in response to your pleas I'll try to add
<a href="DOCUMENTATION.html">documentation</a> to old things that are widely regarded as important.<p>
Second, I worry that the existing <a href="DOCUMENTATION.html">documentation</a> is unhelpful because
it provides too much or too little detail, or it provides the detail
too far away from where it is needed. Please be on the lookout for
this. Did you get what you needed when you appealed to <code>:doc</code> or
<code>:</code><code><a href="MORE-DOC.html">more-doc</a></code>? If not, what was it you needed? Would more
cross-references <a href="HELP.html">help</a>? Did you get lost in maze of
cross-references?
<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>
|
