		Search-engine friendly clone of the ACL2 documentation.

Xdoc::apt-constructors

Xdoc::desc-apt-input-thm-enable

Build a description of the :thm-enable input for the user documentation of an APT transformation.

The wrapper? parameter of this macro has the value :never when the transformation never generates a wrapper; it has the value :optional when the transformation includes a :wrapper input that determines whether the wrapper is generated or not (i.e. the wrapper is optional); it has the value :always when the transformation always generates the wrapper.

This transformation input refers to the theorem that relates the old function to either the new function or the wrapper function, depending on the wrapper? parameter.

Macro: desc-apt-input-thm-enable

(defmacro xdoc::desc-apt-input-thm-enable
          (wrapper? &rest additional)
 (declare
    (xargs :guard (member-eq wrapper? '(:never :optional :always))))
 (b*
  ((thm-name-ref
    (case wrapper?
     (:never "@('old-to-new')")
     (:optional
      "@('old-to-new')
                        (if the @(':wrapper') input is @('nil')) or
                        @('old-to-wrapper')
                        (if the @(':wrapper') input is @('t'))")
     (:always "@('old-to-wrapper')"))))
  (cons
   'xdoc::desc
   (cons
       '"@(':thm-enable') &mdash; default @('t')"
       (cons (cons 'xdoc::p
                   (cons '"Determines whether "
                         (cons thm-name-ref '(" is enabled:"))))
             (cons '(xdoc::ul (xdoc::li "@('t'), to enable it.")
                              (xdoc::li "@('nil'), to disable it."))
                   additional))))))