		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-defn-fundef

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

(defun deftrans-defn-fundef
       (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-fundef))
  (declare (ignorable __function__))
  (deftrans-defn
   'fundef
   names bodies '((fundef fundefp))
   extra-args
   (cons
    'b*
    (cons
     '(((fundef fundef) fundef))
     (cons
      (cons
       'make-fundef
       (cons
        ':extension
        (cons
         'fundef.extension
         (cons
          ':spec
          (cons
           (cons (cdr (assoc-eq 'decl-spec-list names))
                 (cons 'fundef.spec extra-args-names))
           (cons
            ':declor
            (cons
             (cons (cdr (assoc-eq 'declor names))
                   (cons 'fundef.declor extra-args-names))
             (cons
              ':asm?
              (cons
               'fundef.asm?
               (cons
                ':attribs
                (cons
                 'fundef.attribs
                 (cons
                  ':decls
                  (cons
                   (cons (cdr (assoc-eq 'decl-list names))
                         (cons 'fundef.decls extra-args-names))
                   (cons
                    ':body
                    (cons
                         (cons (cdr (assoc-eq 'stmt names))
                               (cons 'fundef.body extra-args-names))
                         'nil)))))))))))))))
      'nil)))
   '(:returns (new-fundef fundefp)))))