• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
      • Evmac-input-hints-p
      • Evmac-input-print-p
      • Event-macro-input-processing
      • Function-definedness
      • Event-macro-screen-printing
      • Make-event-terse
      • Event-macro-applicability-conditions
      • Event-macro-results
      • Template-generators
      • Event-macro-event-generators
      • Event-macro-proof-preparation
      • Try-event
      • Restore-output?
      • Restore-output
      • Fail-event
      • Cw-event
      • Event-macro-xdoc-constructors
        • Event-macro-xdoc-constructors-user-level
          • Xdoc::evmac-desc-function/lambda/macro
          • Xdoc::evmac-desc-term
          • Xdoc::evmac-topic-design-notes
          • Xdoc::evmac-appcond
          • Xdoc::evmac-desc-input-name
          • Xdoc::evmac-section-redundancy
          • Xdoc::evmac-input-show-only
          • Xdoc::evmac-input-print
          • Xdoc::evmac-desc-input-enable-t/nil
          • Xdoc::evmac-section-appconds
          • Xdoc::evmac-input-hints
          • Xdoc::evmac-section-generated
          • Xdoc::evmac-section-intro
          • Xdoc::evmac-section-inputs
          • Xdoc::evmac-section-form
        • Event-macro-xdoc-constructors-implementation-level
      • Event-macro-intro-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Event-macro-xdoc-constructors-user-level

Xdoc::evmac-section-redundancy

Construct the redundancy section of the user documentation of an event macro.

This assumes an event macro with a :print and :show-only inputs with specific meanings. This XDOC constructor may be generalized in the future to cover event macros that do not have exactly those two specific inputs with those specific meanings.

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-redundancy

(defmacro xdoc::evmac-section-redundancy (macro)
 (declare (xargs :guard (symbolp macro)))
 (b* ((macro-name (string-downcase (symbol-name macro)))
      (macro-ref (concatenate 'string
                              "@('" macro-name "')")))
  (cons
   'xdoc::section
   (cons
    'xdoc::*evmac-section-redundancy-title*
    (cons
     (cons
      'xdoc::p
      (cons
       (cons
        'concatenate
        (cons
         ''string
         (cons
          '"A call of "
          (cons
           macro-ref
           (cons
            '" is redundant if and only if
         it is identical to a previous successful call of "
            (cons macro-ref
                  '(" whose @(':show-only') input is not @('t'),
         except that the two calls may differ in
         their @(':print') and @(':show-only') inputs.
         These inputs do not affect the generated events,
         and thus they are ignored for the purpose of redundancy.")))))))
       'nil))
     (cons (cons 'xdoc::p
                 (cons (cons 'concatenate
                             (cons ''string
                                   (cons '"A call of "
                                         (cons macro-ref
                                               '(" whose @(':show-only') input is @('t')
         does not generate any event.
         Thus, no successive call may be redundant with such a call.")))))
                       'nil))
           'nil))))))