Doc
Documentation at the terminal
The :doc command may be used at the ACL2 prompt to access the
ACL2 system documentation. Usually (when the xdoc system has
been included) it can also access other documentation topics defined in the
current session, including via included books. However, most users will
probably access the ACL2 documentation in other ways; see documentation. In particular, consider using the
ACL2+Books Manual, for topics documented in the ACL2 community
books or in the ACL2 system (where the latter are rearranged).
Alternatively, consider using the ACL2-doc Emacs browser; see ACL2-doc.
Examples:
ACL2 !>:doc DEFTHM ; print documentation of DEFTHM
ACL2 !>:doc logical-name ; print documentation of LOGICAL-NAME
General Form:
ACL2>:doc name
Note that links are always printed with respect to the "ACL2"
package (that is, as though the current package were "ACL2"). So for
example, a link to the present topic will be displayed as [doc], not as
[acl2::doc], regardless of the current package or the package of the
topic being displayed. Such links can thus take you to topics in the acl2-doc
Emacs browser (see ACL2-doc).
Note that community-book xdoc/top redefines :doc (using
add-ld-keyword-alias!) to invoke the similar macro xdoc, which can
access documentation topics defined in books.
