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