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:
(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)))))