Generate all the overloaded Java methods for an ACL2 function synonym.
(atj-gen-shallow-synonym-all-methods fn fns-that-may-throw pkg-class-names fn-method-names guards$ wrld) → methods
See atj-gen-shallow-synonym-method first.
We retrieve all the primary and secondary function types of
Function:
(defun atj-gen-shallow-synonym-all-methods (fn fns-that-may-throw pkg-class-names fn-method-names guards$ wrld) (declare (xargs :guard (and (symbolp fn) (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-synonym-all-methods)) (declare (ignorable __function__)) (b* ((fn-info (atj-get-function-type-info fn guards$ wrld)) (main-fn-type (atj-function-type-info->main fn-info)) (other-fn-types (atj-function-type-info->others fn-info)) (all-fn-types (cons main-fn-type other-fn-types))) (atj-gen-shallow-synonym-methods fn fns-that-may-throw all-fn-types pkg-class-names fn-method-names wrld))))
Theorem:
(defthm jmethod-listp-of-atj-gen-shallow-synonym-all-methods (b* ((methods (atj-gen-shallow-synonym-all-methods fn fns-that-may-throw pkg-class-names fn-method-names guards$ wrld))) (jmethod-listp methods)) :rule-classes :rewrite)