		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-pkgs

Generate Java code to build the ACL2 packages.

Signature
(atj-gen-pkgs pkgs) → block
Arguments: pkgs — Guard (string-listp pkgs).
Returns: block — Type (jblockp block).

This is a sequence of calls to the methods generated by atj-gen-pkg-methods. These calls are part of the code that initializes (the Java representation of) the ACL2 environment.

Definitions and Theorems

Function: atj-gen-pkgs

(defun atj-gen-pkgs (pkgs)
  (declare (xargs :guard (string-listp pkgs)))
  (let ((__function__ 'atj-gen-pkgs))
    (declare (ignorable __function__))
    (if (endp pkgs)
        nil
      (b* ((method-name (atj-gen-pkg-method-name (car pkgs)))
           (first-block (jblock-method method-name nil))
           (rest-block (atj-gen-pkgs (cdr pkgs))))
        (append first-block rest-block)))))

Theorem: jblockp-of-atj-gen-pkgs

(defthm jblockp-of-atj-gen-pkgs
  (b* ((block (atj-gen-pkgs pkgs)))
    (jblockp block))
  :rule-classes :rewrite)