• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
      • Std/lists
      • Omaps
      • Std/alists
      • Obags
      • Std/util
        • Defprojection
        • Deflist
        • Defaggregate
        • Define
        • Defmapping
        • Defenum
        • Add-io-pairs
        • Defalist
        • Defmapappend
        • Returns-specifiers
        • Defarbrec
        • Define-sk
        • Defines
        • 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
            • Defmacro+-extract-parents/short/long
            • Defmacro+-fn
            • Defmacro+-macro-definition
          • Defsum
          • Defthm-commutative
          • Definj
          • Defirrelevant
          • Defredundant
        • Std/strings
        • Std/osets
        • Std/io
        • Std/basic
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Defmacro+-implementation

    Defmacro+-macro-definition

    Definition of the defmacro+ macro.

    Macro: defmacro+

    (defmacro defmacro+ (name args &rest rest)
      (cons 'make-event
            (cons (cons 'defmacro+-fn
                        (cons (cons 'quote (cons name 'nil))
                              (cons (cons 'quote (cons args 'nil))
                                    (cons (cons 'quote (cons rest 'nil))
                                          'nil))))
                  'nil)))