(deftrans-defn-specqual names bodies extra-args extra-args-names) → *
Function:
(defun deftrans-defn-specqual (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-specqual)) (declare (ignorable __function__)) (deftrans-defn 'specqual names bodies '((specqual specqualp)) extra-args (cons 'specqual-case (cons 'specqual (cons ':tyspec (cons (cons 'specqual-tyspec (cons (cons (cdr (assoc-eq 'type-spec names)) (cons 'specqual.unwrap extra-args-names)) 'nil)) (cons ':tyqual (cons '(specqual-fix specqual) (cons ':alignspec (cons (cons 'specqual-alignspec (cons (cons (cdr (assoc-eq 'alignspec names)) (cons 'specqual.unwrap extra-args-names)) 'nil)) 'nil)))))))) '(:returns (new-specqual specqualp) :measure (specqual-count specqual)))))