• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Std/util
    • Apt
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
      • Evmac-input-hints-p
      • Function-definedness
      • Event-macro-input-processing
      • Event-macro-screen-printing
      • Evmac-input-print-p
      • 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
        • Event-macro-xdoc-constructors-implementation-level
          • Xdoc::evmac-topic-implementation
          • Xdoc::evmac-topic-event-generation
          • Xdoc::evmac-topic-input-processing
          • Xdoc::evmac-topic-library-extensions
      • 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
  • Testing-utilities
  • Math

• Event-macro-xdoc-constructors

Event-macro-xdoc-constructors-implementation-level

Utilities to construct XDOC strings to document the implementation of event macros.

Subtopics

Xdoc::evmac-topic-implementation

Generate an XDOC topic for the implementation of an event macro.

Xdoc::evmac-topic-event-generation

Generate an XDOC topic for the event generation that is part of the implementation of an event macro.

Xdoc::evmac-topic-input-processing

Generate an XDOC topic for the input processing that is part of the implementation of an event macro.

Xdoc::evmac-topic-library-extensions

Generate an XDOC topic for the library extensions that are part of the implementation of an event macro.