Defxdoc
Add documentation to the xdoc database.
Note: defxdoc is very basic. You will usually want to
use defsection or ACL2::define instead.
Defxdoc is the XDOC alternative to ACL2's built-in defdoc
command.
General form:
(defxdoc name
[:parents parents]
[:short short]
[:long long])
Example:
(defxdoc duplicity
:parents (std/lists defsort count no-duplicatesp)
:short "@(call duplicity) counts how many times the
element @('a') occurs within the string @('x')."
:long "<p>This function is similar to ACL2's built-in
@('count') function but is more limited:</p> ...")
The name of each documentation topic must be a symbol. All of the
keyword arguments are optional:
- parents let you associate this documentation with other topics. A
topic may have many parents, but circular chains of parents are not allowed and
will lead to errors when generating manuals. If no :parents are given
explicitly, the default parents
will be used.
- short should be a short description of this topic that is suitable for
inlining in other pages. For instance, it may be displayed in subtopic listing
and in "hover" text on navigation pages.
- long should be the full, detailed documentation for this topic.
The short and long strings may be written using the XDOC markup language, and may also use preprocessor commands to insert
function definitions, theorems, topic links, and so on.
Many examples of using XDOC can be found throughout the ACL2 books. See for
instance the ACL2::std, ACL2::std/strings or ACL2::std/osets libraries.
Note for Advanced Users
XDOC just stores its documentation in an ordinary ACL2 table, so if you want
to do something like automatically generate documentation from macros, you
might decide to bypass defxdoc and just manipulate the table directly.
It is not possible to directly use defxdoc from raw Lisp, but you can
use defxdoc-raw instead.
Subtopics
- Defxdoc+
- defxdoc+ extends defxdoc with some conveniences.
