Lift atj-gen-shallow-fnnative-method to lists of function types.
(atj-gen-shallow-fnnative-methods fn fns-that-may-throw fn-types method-name method-param-names method-body) → methods
Function:
(defun atj-gen-shallow-fnnative-methods (fn fns-that-may-throw fn-types method-name method-param-names method-body) (declare (xargs :guard (and (symbolp fn) (symbol-listp fns-that-may-throw) (atj-function-type-listp fn-types) (stringp method-name) (string-listp method-param-names) (jblockp method-body)))) (declare (xargs :guard (aij-nativep fn))) (let ((__function__ 'atj-gen-shallow-fnnative-methods)) (declare (ignorable __function__)) (cond ((endp fn-types) nil) (t (cons (atj-gen-shallow-fnnative-method fn fns-that-may-throw (car fn-types) method-name method-param-names method-body) (atj-gen-shallow-fnnative-methods fn fns-that-may-throw (cdr fn-types) method-name method-param-names method-body))))))
Theorem:
(defthm jmethod-listp-of-atj-gen-shallow-fnnative-methods (b* ((methods (atj-gen-shallow-fnnative-methods fn fns-that-may-throw fn-types method-name method-param-names method-body))) (jmethod-listp methods)) :rule-classes :rewrite)