Major Section: ACL2 Documentation
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.
For an introduction to the ACL2 online documentation system, type
more below. Whenever the documentation system concludes with
``(type :more for more, :more! for the rest)'' you may type
to see the next block of documentation.
Topics related to documentation are documented individually:
constraint, etc., of a function symbol
If there is some name you wish to know more about, then type
ACL2 !>:doc namein 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,
Every name that is documented contains a one-line description, a few
notes, and some details.
Doc will print the one-liner and the
doc 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
ACL2 !>:morea 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 ``
*-'' if the text has been exhausted. By continuing to type
moreuntil exhausting the text you can read successive blocks. Alternatively, you can type
more!to get all the remaining blocks.
If you want to get the details and don't want to see the elementary
stuff typed by
doc name, type:
ACL2 !>:MORE-DOC nameWe have documented not just function names but names of certain important ideas too. For example, see rewrite and see meta to learn about
metarules, respectively. See hints to learn about the structure of the
hintsargument to the prover. The
deflabelevent (see deflabel) is a way to introduce a logical name for no reason other than to attach documentation to it; also see defdoc.
How do you know what names are documented? There is a documentation
data base which is querried with the
The documentation data base is divided into sections. The sections are listed by
ACL2 !>:docs *Each section has a name,
sect, and by typing
ACL2 !>:docs sector equivalently
ACL2 !>:doc sectyou will get an enumeration of the topics within that section. Those topics can be further explored by using
more) on them. In fact the section name itself is just a documented name.
moregenerally gives an informal overview of the general subject of the section.
ACL2 !>:docs **will list all documented topics, by section. This fills several pages but might be a good place to start.
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 ``
ACL2 !>:docs "functional inst"will list every documented topic whose
more-doctext includes the substring
"functional inst", where case and the exact number of spaces are irrelevant.
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.
ACL2 !>:args fnwill 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
fnis defined as a function or macro.
You might also want to type:
ACL2 !>:pc fnwhich will print the command which introduced
fn. You should see command-descriptor for details on the kinds of input you can give the
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.
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
:doc-section''. When such a documentation string is
seen, it is stored in the data base and may be displayed via
docs, etc. Such documentation strings must follow rigid
syntactic rules to permit their processing by our commands. These
are spelled out elsewhere; see doc-string.
A description of the structure of the documentation data base may
also be found; see doc-string.