		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-pkg-method-name

Name of the Java method that adds an ACL2 package definition.

Signature
(atj-gen-pkg-method-name pkg) → method-name
Arguments: pkg — Guard (stringp pkg).
Returns: method-name — Type (stringp method-name).

We generate a private static method for each ACL2 package definition to build. This function generates the name of this method, which is distinct from all the other methods generated for the same class.

Definitions and Theorems

Function: atj-gen-pkg-method-name

(defun atj-gen-pkg-method-name (pkg)
  (declare (xargs :guard (stringp pkg)))
  (let ((__function__ 'atj-gen-pkg-method-name))
    (declare (ignorable __function__))
    (str::cat "addPackageDef_"
              (implode (atj-chars-to-jchars-id (explode pkg)
                                               nil
                                               :dash nil)))))

Theorem: stringp-of-atj-gen-pkg-method-name

(defthm stringp-of-atj-gen-pkg-method-name
  (b* ((method-name (atj-gen-pkg-method-name pkg)))
    (stringp method-name))
  :rule-classes :rewrite)