		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-defn-member-designor

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

(defun deftrans-defn-member-designor
       (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-member-designor))
  (declare (ignorable __function__))
  (deftrans-defn
   'member-designor
   names
   bodies '((memdes member-designorp))
   extra-args
   (cons
    'member-designor-case
    (cons
     'memdes
     (cons
      ':ident
      (cons
       '(member-designor-fix memdes)
       (cons
        ':dot
        (cons
         (cons
           'make-member-designor-dot
           (cons ':member
                 (cons (cons (cdr (assoc-eq 'member-designor names))
                             (cons 'memdes.member extra-args-names))
                       '(:name memdes.name))))
         (cons
          ':sub
          (cons
           (cons
            'make-member-designor-sub
            (cons
             ':member
             (cons
              (cons (cdr (assoc-eq 'member-designor names))
                    (cons 'memdes.member extra-args-names))
              (cons
                  ':index
                  (cons (cons (cdr (assoc-eq 'expr names))
                              (cons 'memdes.index extra-args-names))
                        'nil)))))
           'nil))))))))
   '(:returns (new-memdes member-designorp)
              :measure (member-designor-count memdes)))))