		Search-engine friendly clone of the ACL2 documentation.

Event-macro-xdoc-constructors-user-level

Xdoc::evmac-section-appconds

Construct the applicability conditions section of the user documentation of an event macro.

Since this documentation is part of the XDOC topic whose name is the name of the macro, the macro-ref variable is not a link.

Macro: evmac-section-appconds

(defmacro xdoc::evmac-section-appconds (macro &rest content)
 (declare (xargs :guard (symbolp macro)))
 (b*
   ((macro-name (string-downcase (symbol-name macro)))
    (macro-ref (concatenate 'string
                            "@('" macro-name "')"))
    (inputs-ref (concatenate 'string
                             "`" xdoc::*evmac-section-inputs-title*
                             "' section")))
  (cons
   'xdoc::section
   (cons
    'xdoc::*evmac-section-appconds-title*
    (cons
     (cons
      'xdoc::p
      (cons
       '"In order for "
       (cons
        macro-ref
        (cons
         '" to apply,
        in addition to the requirements on the inputs
        stated in the "
         (cons
          inputs-ref
          (cons
           '", the following "
           (cons
            '(xdoc::seetopic
                  "acl2::event-macro-applicability-conditions"
                  "applicability conditions")
            (cons
             '" must be proved.
         The proofs are attempted when "
             (cons
              macro-ref
              (cons
               '" is called,
        using the hints optionally supplied as the @(':hints') input
        described in the "
               (cons inputs-ref '("."))))))))))))
     content)))))