		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-defn-initdeclor

Signature
(deftrans-defn-initdeclor names bodies extra-args extra-args-names) → *
Arguments: names — Guard (alistp names).; bodies — Guard (alistp bodies).; extra-args — Guard (true-listp extra-args).; extra-args-names — Guard (true-listp extra-args-names).

Definitions and Theorems

Function: deftrans-defn-initdeclor

(defun deftrans-defn-initdeclor
       (names bodies extra-args extra-args-names)
 (declare (xargs :guard (and (alistp names)
                             (alistp bodies)
                             (true-listp extra-args)
                             (true-listp extra-args-names))))
 (let ((__function__ 'deftrans-defn-initdeclor))
  (declare (ignorable __function__))
  (deftrans-defn
   'initdeclor
   names bodies '((initdeclor initdeclorp))
   extra-args
   (cons
    'b*
    (cons
     '(((initdeclor initdeclor) initdeclor))
     (cons
      (cons
       'make-initdeclor
       (cons
        ':declor
        (cons
         (cons (cdr (assoc-eq 'declor names))
               (cons 'initdeclor.declor
                     extra-args-names))
         (cons
          ':asm?
          (cons
           'initdeclor.asm?
           (cons
            ':attribs
            (cons
             'initdeclor.attribs
             (cons ':init?
                   (cons (cons (cdr (assoc-eq 'initer-option names))
                               (cons 'initdeclor.init?
                                     extra-args-names))
                         'nil)))))))))
      'nil)))
   '(:returns (new-initdeclor initdeclorp)
              :measure (initdeclor-count initdeclor)))))