		Search-engine friendly clone of the ACL2 documentation.

Atj-library-extensions

Atj-string-ascii-java-package-name-p

Check if an ACL2 string is a valid ASCII Java package name.

Signature
(atj-string-ascii-java-package-name-p string) → yes/no
Arguments: string — Guard (stringp string).
Returns: yes/no — Type (booleanp yes/no).

The string must consist of one or more ASCII Java identifiers separated by dots.

Definitions and Theorems

Function: atj-string-ascii-java-package-name-p

(defun atj-string-ascii-java-package-name-p (string)
  (declare (xargs :guard (stringp string)))
  (let ((__function__ 'atj-string-ascii-java-package-name-p))
    (declare (ignorable __function__))
    (b* ((identifiers (str::strtok! string (list #\.))))
      (and (consp identifiers)
           (atj-string-ascii-java-identifier-listp identifiers)))))

Theorem: booleanp-of-atj-string-ascii-java-package-name-p

(defthm booleanp-of-atj-string-ascii-java-package-name-p
  (b* ((yes/no (atj-string-ascii-java-package-name-p string)))
    (booleanp yes/no))
  :rule-classes :rewrite)