		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-defn-decl

Signature
(deftrans-defn-decl 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-decl

(defun deftrans-defn-decl (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-decl))
  (declare (ignorable __function__))
  (deftrans-defn
   'decl
   names bodies '((decl declp))
   extra-args
   (cons
    'decl-case
    (cons
     'decl
     (cons
      ':decl
      (cons
       (cons
        'make-decl-decl
        (cons
         ':extension
         (cons
          'decl.extension
          (cons
           ':specs
           (cons
            (cons (cdr (assoc-eq 'decl-spec-list names))
                  (cons 'decl.specs extra-args-names))
            (cons
                 ':init
                 (cons (cons (cdr (assoc-eq 'initdeclor-list names))
                             (cons 'decl.init extra-args-names))
                       'nil)))))))
       (cons
        ':statassert
        (cons
             (cons 'decl-statassert
                   (cons (cons (cdr (assoc-eq 'statassert names))
                               (cons 'decl.unwrap extra-args-names))
                         'nil))
             'nil))))))
   '(:returns (new-decl declp)
              :measure (decl-count decl)))))