		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-process-java-package

Process the :java-package input.

Signature
(atj-process-java-package java-package ctx state) → (mv erp nothing state)
Arguments: ctx — Guard (ctxp ctx).
Returns: nothing — Type (null nothing).

Definitions and Theorems

Function: atj-process-java-package

(defun atj-process-java-package (java-package ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (ctxp ctx)))
 (let ((__function__ 'atj-process-java-package))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (ensure-string-or-nil$ java-package
                            "The :JAVA-PACKAGE input" t nil))
    ((unless
          (or (null java-package)
              (atj-string-ascii-java-package-name-p java-package)))
     (er-soft+
      ctx t nil
      "The :JAVA-PACKAGE input ~x0 is not ~
                   NIL or a valid Java package name ~
                   consisting of only ASCII characters."
      java-package))
    ((when (equal java-package *aij-package*))
     (er-soft+
      ctx t nil
      "The :JAVA-PACKAGE input ~x0 must differ from ~
                   the name of the Java package of AIJ ~x1."
      java-package *aij-package*)))
   (value nil))))

Theorem: null-of-atj-process-java-package.nothing

(defthm null-of-atj-process-java-package.nothing
  (b* (((mv ?erp ?nothing acl2::?state)
        (atj-process-java-package java-package ctx state)))
    (null nothing))
  :rule-classes :rewrite)