		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-defn-genassoc

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

(defun deftrans-defn-genassoc
       (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-genassoc))
  (declare (ignorable __function__))
  (deftrans-defn
   'genassoc
   names bodies '((genassoc genassocp))
   extra-args
   (cons
    'genassoc-case
    (cons
     'genassoc
     (cons
      ':type
      (cons
       (cons
        'make-genassoc-type
        (cons
         ':type
         (cons
           (cons (cdr (assoc-eq 'tyname names))
                 (cons 'genassoc.type extra-args-names))
           (cons ':expr
                 (cons (cons (cdr (assoc-eq 'expr names))
                             (cons 'genassoc.expr extra-args-names))
                       'nil)))))
       (cons
        ':default
        (cons
           (cons 'genassoc-default
                 (cons (cons (cdr (assoc-eq 'expr names))
                             (cons 'genassoc.expr extra-args-names))
                       'nil))
           'nil))))))
   '(:returns (new-genassoc genassocp)
              :measure (genassoc-count genassoc)))))