		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-string-field

Generate a Java field for an ACL2 quoted string.

Signature
(atj-gen-shallow-string-field string) → field
Arguments: string — Guard (stringp string).
Returns: field — Type (jfieldp field).

This is a private static final field with an initializer, which constructs the string value.

Definitions and Theorems

Function: atj-gen-shallow-string-field

(defun atj-gen-shallow-string-field (string)
  (declare (xargs :guard (stringp string)))
  (let ((__function__ 'atj-gen-shallow-string-field))
    (declare (ignorable __function__))
    (b* ((name (atj-gen-shallow-string-field-name string))
         (init (atj-gen-string string t nil))
         (type *aij-type-string*))
      (make-jfield :access (jaccess-private)
                   :static? t
                   :final? t
                   :transient? nil
                   :volatile? nil
                   :type type
                   :name name
                   :init? init))))

Theorem: jfieldp-of-atj-gen-shallow-string-field

(defthm jfieldp-of-atj-gen-shallow-string-field
  (b* ((field (atj-gen-shallow-string-field string)))
    (jfieldp field))
  :rule-classes :rewrite)