• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • 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
          • 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+-fn

Event generated by defmacro+.

Definitions and Theorems

Function: defmacro+-fn

(defun defmacro+-fn (name args rest)
 (declare (xargs :guard (and (symbolp name) (true-listp rest))))
 (if
  (symbolp name)
  (mv-let (alist rest)
          (defmacro+-find-parents/short/long rest)
   (let ((parents-pair (assoc-eq :parents alist))
         (short-pair (assoc-eq :short alist))
         (long-pair (assoc-eq :long alist))
         (name-ref (concatenate 'string
                                (symbol-package-name name)
                                "::" (symbol-name name))))
    (cons
     'defsection
     (cons
      name
      (append
       (and parents-pair
            (list :parents (cdr parents-pair)))
       (append
        (and short-pair
             (list :short (cdr short-pair)))
        (append
         (if long-pair
          (list
           :long (cons 'concatenate
                       (cons ''string
                             (cons (cdr long-pair)
                                   (cons '"@(def "
                                         (cons name-ref '(")")))))))
          (list :long (cons 'concatenate
                            (cons ''string
                                  (cons '"@(def "
                                        (cons name-ref '(")")))))))
         (cons (cons 'defmacro
                     (cons name (cons args rest)))
               'nil))))))))
  (er hard? 'defmacro+
      "The first argument ~x0 must be a symbol."
      name)))