Lift atj-gen-shallow-synonym-all-methods to lists of functions.
(atj-gen-shallow-all-synonym-methods fns fns-that-may-throw pkg-class-names fn-method-names guards$ wrld) → methods
Function:
(defun atj-gen-shallow-all-synonym-methods (fns fns-that-may-throw pkg-class-names fn-method-names guards$ wrld) (declare (xargs :guard (and (symbol-listp fns) (symbol-listp fns-that-may-throw) (string-string-alistp pkg-class-names) (symbol-string-alistp fn-method-names) (booleanp guards$) (plist-worldp wrld)))) (let ((__function__ 'atj-gen-shallow-all-synonym-methods)) (declare (ignorable __function__)) (cond ((endp fns) nil) (t (append (atj-gen-shallow-synonym-all-methods (car fns) fns-that-may-throw pkg-class-names fn-method-names guards$ wrld) (atj-gen-shallow-all-synonym-methods (cdr fns) fns-that-may-throw pkg-class-names fn-method-names guards$ wrld))))))
Theorem:
(defthm jmethod-listp-of-atj-gen-shallow-all-synonym-methods (b* ((methods (atj-gen-shallow-all-synonym-methods fns fns-that-may-throw pkg-class-names fn-method-names guards$ wrld))) (jmethod-listp methods)) :rule-classes :rewrite)