		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-pkg-methods

Generate all the Java methods that add the ACL2 package definitions.

Signature
(atj-gen-pkg-methods pkgs verbose$) → methods
Arguments: pkgs — Guard (string-listp pkgs).; verbose$ — Guard (booleanp verbose$).
Returns: methods — Type (jmethod-listp methods).

Definitions and Theorems

Function: atj-gen-pkg-methods

(defun atj-gen-pkg-methods (pkgs verbose$)
  (declare (xargs :guard (and (string-listp pkgs)
                              (booleanp verbose$))))
  (let ((__function__ 'atj-gen-pkg-methods))
    (declare (ignorable __function__))
    (if (endp pkgs)
        nil
      (b* ((first-method (atj-gen-pkg-method (car pkgs)
                                             verbose$))
           (rest-methods (atj-gen-pkg-methods (cdr pkgs)
                                              verbose$)))
        (cons first-method rest-methods)))))

Theorem: jmethod-listp-of-atj-gen-pkg-methods

(defthm jmethod-listp-of-atj-gen-pkg-methods
  (b* ((methods (atj-gen-pkg-methods pkgs verbose$)))
    (jmethod-listp methods))
  :rule-classes :rewrite)