		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-defn-paramdeclor

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

(defun deftrans-defn-paramdeclor
       (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-paramdeclor))
  (declare (ignorable __function__))
  (deftrans-defn
   'paramdeclor
   names
   bodies '((paramdeclor paramdeclorp))
   extra-args
   (cons
    'paramdeclor-case
    (cons
     'paramdeclor
     (cons
      ':declor
      (cons
       (cons 'paramdeclor-declor
             (cons (cons (cdr (assoc-eq 'declor names))
                         (cons 'paramdeclor.unwrap
                               extra-args-names))
                   'nil))
       (cons
        ':absdeclor
        (cons
          (cons 'paramdeclor-absdeclor
                (cons (cons (cdr (assoc-eq 'absdeclor names))
                            (cons 'paramdeclor.unwrap
                                  extra-args-names))
                      'nil))
          '(:none
                (paramdeclor-none)
                :ambig (prog2$ (raise "Misusage error: ~x0."
                                      (paramdeclor-fix paramdeclor))
                               (paramdeclor-fix paramdeclor)))))))))
   '(:returns (new-paramdeclor paramdeclorp)
              :measure (paramdeclor-count paramdeclor)))))