		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-defn-desiniter

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

(defun deftrans-defn-desiniter
       (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-desiniter))
  (declare (ignorable __function__))
  (deftrans-defn
   'desiniter
   names bodies '((desiniter desiniterp))
   extra-args
   (cons
    'b*
    (cons
     '(((desiniter desiniter) desiniter))
     (cons
      (cons
        'make-desiniter
        (cons ':designors
              (cons (cons (cdr (assoc-eq 'designor-list names))
                          (cons 'desiniter.designors
                                extra-args-names))
                    (cons ':initer
                          (cons (cons (cdr (assoc-eq 'initer names))
                                      (cons 'desiniter.initer
                                            extra-args-names))
                                'nil)))))
      'nil)))
   '(:returns (new-desiniter desiniterp)
              :measure (desiniter-count desiniter)))))