		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-static-initializer

Generate the static initializer of the main Java class.

Signature
(atj-gen-static-initializer java-class$) → initializer
Arguments: java-class$ — Guard (stringp java-class$).
Returns: initializer — Type (jcinitializerp initializer).

This calls the build() method of the environment Java class.

Definitions and Theorems

Function: atj-gen-static-initializer

(defun atj-gen-static-initializer (java-class$)
 (declare (xargs :guard (stringp java-class$)))
 (let ((__function__ 'atj-gen-static-initializer))
  (declare (ignorable __function__))
  (make-jcinitializer
       :static? t
       :code (jblock-smethod
                  (jtype-class (str::cat java-class$ "Environment"))
                  "build" nil))))

Theorem: jcinitializerp-of-atj-gen-static-initializer

(defthm jcinitializerp-of-atj-gen-static-initializer
  (b* ((initializer (atj-gen-static-initializer java-class$)))
    (jcinitializerp initializer))
  :rule-classes :rewrite)