		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-char-field

Generate a Java field for an ACL2 quoted character.

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

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

Definitions and Theorems

Function: atj-gen-shallow-char-field

(defun atj-gen-shallow-char-field (char)
  (declare (xargs :guard (characterp char)))
  (let ((__function__ 'atj-gen-shallow-char-field))
    (declare (ignorable __function__))
    (b* ((name (atj-gen-shallow-char-field-name char))
         (init (atj-gen-char char t nil))
         (type *aij-type-char*))
      (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-char-field

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