		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-cons-field

Generate a Java field for an ACL2 quoted cons pair.

Signature
(atj-gen-shallow-cons-field cons qpairs) → field
Arguments: cons — Guard (consp cons).; qpairs — Guard (cons-pos-alistp qpairs).
Returns: field — Type (jfieldp field).

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

Definitions and Theorems

Function: atj-gen-shallow-cons-field

(defun atj-gen-shallow-cons-field (cons qpairs)
  (declare (xargs :guard (and (consp cons)
                              (cons-pos-alistp qpairs))))
  (let ((__function__ 'atj-gen-shallow-cons-field))
    (declare (ignorable __function__))
    (b* ((name (atj-gen-shallow-cons-field-name cons qpairs))
         (init (atj-gen-value-flat cons))
         (type *aij-type-cons*))
      (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-cons-field

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