• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
      • Apt
      • Std/util
        • Defprojection
        • Deflist
        • Defaggregate
        • Define
        • Defmapping
        • Defenum
        • Add-io-pairs
        • Defalist
        • Defmapappend
        • Returns-specifiers
        • Defarbrec
        • Defines
        • Define-sk
        • Error-value-tuples
        • Defmax-nat
        • Defmin-int
        • Deftutorial
        • Extended-formals
        • Defrule
        • Defval
        • Defsurj
        • Defiso
        • Defconstrained-recognizer
        • Deffixer
        • Defmvtypes
        • Defconsts
        • Defthm-unsigned-byte-p
        • Support
        • Defthm-signed-byte-p
        • Defthm-natp
        • Defund-sk
        • Defmacro+
          • Defmacro+-implementation
        • Defsum
        • Defthm-commutative
        • Definj
        • Defirrelevant
        • Defredundant
      • Defdata
      • Defrstobj
      • Seq
      • Match-tree
      • Defrstobj
      • With-supporters
      • Def-partial-measure
      • Template-subst
      • Soft
      • Defthm-domain
      • Event-macros
      • Def-universal-equiv
      • Def-saved-obligs
      • With-supporters-after
      • Definec
      • Sig
      • Outer-local
      • Data-structures
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
        • Make-event
        • Defmacro
        • Untranslate-patterns
        • Tc
        • Trans*
        • Macro-aliases-table
        • Macro-args
        • Defabbrev
        • User-defined-functions-table
        • Trans
        • Untranslate-for-execution
        • Add-macro-fn
        • Check-vars-not-free
        • Safe-mode
        • Macro-libraries
          • B*
          • Defunc
          • Fty
          • Apt
          • Std/util
            • Defprojection
            • Deflist
            • Defaggregate
            • Define
            • Defmapping
            • Defenum
            • Add-io-pairs
            • Defalist
            • Defmapappend
            • Returns-specifiers
            • Defarbrec
            • Defines
            • Define-sk
            • Error-value-tuples
            • Defmax-nat
            • Defmin-int
            • Deftutorial
            • Extended-formals
            • Defrule
            • Defval
            • Defsurj
            • Defiso
            • Defconstrained-recognizer
            • Deffixer
            • Defmvtypes
            • Defconsts
            • Defthm-unsigned-byte-p
            • Support
            • Defthm-signed-byte-p
            • Defthm-natp
            • Defund-sk
            • Defmacro+
              • Defmacro+-implementation
            • Defsum
            • Defthm-commutative
            • Definj
            • Defirrelevant
            • Defredundant
          • Defdata
          • Defrstobj
          • Seq
          • Match-tree
          • Defrstobj
          • With-supporters
          • Def-partial-measure
          • Template-subst
          • Soft
          • Defthm-domain
          • Event-macros
          • Def-universal-equiv
          • Def-saved-obligs
          • With-supporters-after
          • Definec
          • Sig
          • Outer-local
          • Data-structures
        • Trans1
        • Defmacro-untouchable
        • Set-duplicate-keys-action
        • Add-macro-alias
        • Magic-macroexpand
        • Defmacroq
        • Trans!
        • Remove-macro-fn
        • Remove-macro-alias
        • Add-binop
        • Untrans-table
        • Trans*-
        • Remove-binop
        • Tcp
        • Tca
      • Interfacing-tools
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Std/util
  • Defmacro

Defmacro+

An enhancement of defmacro with XDOC integration.

This is like defmacro, but it also allows the user to include keyword options :parents, :short, and :long. None, some, or all those keywords may be present, in any order, and anywhere after the macro arguments.

Besides generating the defmacro obtained by removing those keyword options, defmacro+ also generates a defsection around the macro, with the specified parents, short string, and long string, if any. The long string is augmented with a @(def ...) for the macro.

Subtopics

Defmacro+-implementation
Implementation of defmacro+.