		Search-engine friendly clone of the ACL2 documentation.

Event-macro-xdoc-constructors-user-level

Xdoc::evmac-input-hints

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

Macro: evmac-input-hints

(defmacro xdoc::evmac-input-hints (&key additional)
 (let ((appconds-ref
            (concatenate 'string
                         "`" xdoc::*evmac-section-appconds-title*
                         "' section")))
  (cons
   'xdoc::desc
   (cons
    '"@(':hints') &mdash; 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)))))))