Construct a description of the
Macro:
(defmacro xdoc::evmac-input-hints (&key additional) (let ((appconds-ref (concatenate 'string "`" xdoc::*evmac-section-appconds-title* "' section"))) (cons 'xdoc::desc (cons '"@(':hints') — default @('nil')" (cons '(xdoc::p "Hints to prove the applicability conditions.") (cons '(xdoc::p "It must be one of the following:") (cons (cons 'xdoc::ul (cons (cons 'xdoc::li (cons '"A " (cons '(xdoc::seetopic "acl2::keyword-value-listp" "keyword-value list") (cons '" @('(appcond1 hints1 appcond2 hints2 ...)'), where each @('appcondk') is a keyword that identifies one of the applicability conditions listed in the " (cons appconds-ref (cons '" and each @('hintsk') is a list of hints of the kind that may appear just after @(':hints') in a @(tsee defthm). The hints @('hintsk') are used to prove applicability condition @('appcondk'). The @('appcond1'), @('appcond2'), ... keywords must be all distinct. An @('appcondk') keyword is allowed only if the corresponding applicability condition is present, as specified in the " (cons appconds-ref '(".")))))))) '((xdoc::li "A list of hints of the kind that may appear just after @(':hints') in a @(tsee defthm). In this case, these same hints are used to prove every applicability condition,.")))) additional)))))))