		Search-engine friendly clone of the ACL2 documentation.

Xdoc::apt-constructors

Utilities to construct XDOC strings to document APT transformations.

The xdoc::desc-apt-input-... utilities construct descriptions of inputs common to multiple APT transformations. Each such utility includes zero or more parameters to customize the description, as well as zero or more additional items (e.g. paragraphs) that are appended to the end of the generated description.

Subtopics

Xdoc::desc-apt-input-thm-name: Build a description of the :thm-name input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-thm-enable: Build a description of the :thm-enable input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-verify-guards: Build a description of the :verify-guards input for the user documentation of an APT transformation.
Xdoc::apt-design-notes-ref: Builds text that references the design notes of an APT transformation.
Xdoc::desc-apt-input-wrapper-to-old-name: Build a description of the :wrapper-to-old-name input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-old-to-wrapper-name: Build a description of the :old-to-wrapper-name input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-wrapper-to-old-enable: Build a description of the :wrapper-to-old-enable input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-wrapper-name: Build a description of the :wrapper-name input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-old-to-wrapper-enable: Build a description of the :old-to-wrapper-enable input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-old-to-new-name: Build a description of the :old-to-new-name input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-old-if-new-name: Build a description of the :old-if-new-name input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-new-to-old-name: Build a description of the :new-to-old-name input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-wrapper-enable: Build a description of the :wrapper-enable input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-old-to-new-enable: Build a description of the :old-to-new-enable input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-old-if-new-enable: Build a description of the :old-if-new-enable input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-new-to-old-enable: Build a description of the :new-to-old-enable input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-new-name: Build a description of the :new-name input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-untranslate: Build a description of the :untranslate input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-old: Build a description of the old input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-new-enable: Build a description of the :new-enable input for the user documentation of an APT transformation.
Xdoc::desc-apt-input-wrapper: Build a description of the :wrapper input for the user documentation of an APT transformation.