Major Section: DOCUMENTATION
:doc 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
that comes with the ACL2 distribution.
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" 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 General Form: ACL2>:doc logical-namewhere
logical-nameis a logical name (see logical-name) for which you hope there is documentation. Chances are there is no documentation at the moment, but we are working on adding documentation strings for all the user level ACL2 functions.
For a general discussion of our treatment of documentation strings, see documentation.
This is the first cut at online documentation. Users can be particularly helpful by sending mail on the inadequacies of the system. Address it just to Moore and put Documentation in the subject line. There are several things that trouble me about what I've done here.
First, many concepts aren't documented. Ultimately, I'd like to
. document (a) every CLTL primitive (e.g.,
coerce) and (b)
every ACL2 extension (e.g.,
getprop). But so far I have
focussed on documenting (c) the ACL2 system primitives (e.g.,
hints look like). My priorities are (c), then (b), and
then (a), following the philosophy that the most unstable features
should get online documentation in these early releases. Having
gotten the basic documentation in place, I'll document new things as
they are added, and in response to your pleas I'll try to add
documentation to old things that are widely regarded as important.
Second, I worry that the existing documentation 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
more-doc? If not, what was it you needed? Would more
cross-references help? Did you get lost in maze of