DOCUMENTATION

functions that display documentation at the terminal 
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 :more to see the next block of documentation.

Topics related to documentation are documented individually:

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.

If there is some name you wish to know more about, then type 

ACL2 !>:doc name
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, nil is returned.

Every name that is documented contains a one-line description, a few notes, and some details. :Doc will print the one-liner and the notes. When :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 !>:more
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 ``*-'' if the text has been exhausted. By continuing to type :more until 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 name
We have documented not just function names but names of certain important ideas too. For example, see rewrite and see meta to learn about :rewrite rules and :meta rules, respectively. See hints to learn about the structure of the :hints argument to the prover. The deflabel event (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 :docs command.

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 sect
or equivalently 
ACL2 !>:doc sect
you will get an enumeration of the topics within that section. Those topics can be further explored by using :doc (and :more) on them. In fact the section name itself is just a documented name. :more generally 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 ``apropos'' command. 

ACL2 !>:docs "functional inst"
will list every documented topic whose :doc or :more-doc text 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 fn
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 fn is defined as a function or macro.

You might also want to type: 

ACL2 !>:pc fn
which will print the command which introduced fn. You should see command-descriptor for details on the kinds of input you can give the :pc command.

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 characters ``:doc-section''. When such a documentation string is seen, it is stored in the data base and may be displayed via :doc, :more, :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.