		Search-engine friendly clone of the ACL2 documentation.

Xdoc

Defpointer

Define an alias for a documentation topic.

Examples:

(defpointer acl2s acl2-sedan)
(defpointer guard-hints xargs t)

General Form:

(defpointer new-topic target-topic [keyword-p])

This is a simple macro that expands to a defxdoc form. It introduces a new xdoc topic, new-topic, that merely links to target-topic. The new topic will only be listed under pointers.

A common practice when documenting keyword symbols is to create a doc topic in in the "ACL2" package or some other relevant package, rather than the "KEYWORD" package to which the keyword symbol rightfully belongs. In keeping with this practice, the keywordp argument to defpointer, if non-nil, adds a clarification that the doc topic is really about the keyword symbol with the same name as new-topic, rather than new-topic itself.