(deftrans-defn-extdecl-list names bodies extra-args extra-args-names) → *
Function:
(defun deftrans-defn-extdecl-list (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-extdecl-list)) (declare (ignorable __function__)) (deftrans-defn 'extdecl-list names bodies '((extdecls extdecl-listp)) extra-args (cons 'if (cons '(endp extdecls) (cons 'nil (cons (cons 'cons (cons (cons (cdr (assoc-eq 'extdecl names)) (cons '(car extdecls) extra-args-names)) (cons (cons (cdr (assoc-eq 'extdecl-list names)) (cons '(cdr extdecls) extra-args-names)) 'nil))) 'nil)))) '(:returns (new-extdecls extdecl-listp) :measure (acl2-count extdecls) :hints (("Goal" :in-theory nil))))))