		Search-engine friendly clone of the ACL2 documentation.

Event-macro-xdoc-constructors-user-level

Xdoc::evmac-desc-input-enable-t/nil

Construct a description of a :...-enable input for the user documentation of an event macro.

This is for an input to determine the enablement of an entity (e.g. a function) generated by the event macro.

The ... in :...-enable is passed as the prefix argument of this macro.

The default is passed as the default argument of this macro.

The description of the entity is passed as the desc argument of this macro.

Macro: evmac-desc-input-enable-t/nil

(defmacro xdoc::evmac-desc-input-enable-t/nil
          (prefix &key default desc)
 (declare (xargs :guard (and (stringp prefix)
                             (booleanp default)
                             (stringp desc))))
 (cons
    'xdoc::desc
    (cons (concatenate 'string
                       "@(':"
                       prefix "-enable') &mdash; default "
                       (if default "@('t')" "@('nil')"))
          (cons (cons 'xdoc::p
                      (cons '"Determines whether "
                            (cons desc '(" is enabled."))))
                '((xdoc::p "It must be one of the following:")
                  (xdoc::ul (xdoc::li "@('t'), to enable.")
                            (xdoc::li "@('nil'), to disable.")))))))