Generate all the Java methods to run the specified tests.
(atj-gen-test-methods tests$ deep$ guards$ no-aij-types$ java-class$ verbose$ pkg-class-names fn-method-names wrld) → methods
These are generated only if the
Function:
(defun atj-gen-test-methods (tests$ deep$ guards$ no-aij-types$ java-class$ verbose$ pkg-class-names fn-method-names wrld) (declare (xargs :guard (and (atj-test-listp tests$) (booleanp deep$) (booleanp guards$) (booleanp no-aij-types$) (stringp java-class$) (booleanp verbose$) (string-string-alistp pkg-class-names) (symbol-string-alistp fn-method-names) (plist-worldp wrld)))) (let ((__function__ 'atj-gen-test-methods)) (declare (ignorable __function__)) (if (endp tests$) nil (b* ((first-method (atj-gen-test-method (car tests$) deep$ guards$ no-aij-types$ java-class$ verbose$ pkg-class-names fn-method-names wrld)) (rest-methods (atj-gen-test-methods (cdr tests$) deep$ guards$ no-aij-types$ java-class$ verbose$ pkg-class-names fn-method-names wrld))) (cons first-method rest-methods)))))
Theorem:
(defthm jmethod-listp-of-atj-gen-test-methods (b* ((methods (atj-gen-test-methods tests$ deep$ guards$ no-aij-types$ java-class$ verbose$ pkg-class-names fn-method-names wrld))) (jmethod-listp methods)) :rule-classes :rewrite)