		Search-engine friendly clone of the ACL2 documentation.

Xdoc::apt-constructors

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.

Macro: desc-apt-input-wrapper-to-old-enable

(defmacro xdoc::desc-apt-input-wrapper-to-old-enable nil
 '(xdoc::desc
   "@(':wrapper-to-old-enable') &mdash;
     default from <see topic='@(url defaults-table)'>table</see>"
   (xdoc::p
    "Determines whether the @('wrapper-to-old') theorem is enabled.")
   (xdoc::p "It must be one of the following:")
   (xdoc::ul
    (xdoc::li "@('t'), to enable the theorem.")
    (xdoc::li "@('nil'), to disable the theorem.")
    (xdoc::li
     "Absent, to use the value from the APT defaults table,
       which is set via @(tsee set-default-input-wrapper-to-old-enable)."))
   (xdoc::p
    "This input may be present only if the @(':wrapper') input is @('t').")
   (xdoc::p
    "If this input is @('t'),
      the @(':old-to-wrapper-enable') input must be @('nil').
      At most one of these two inputs may be @('t') at any time.")))