		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-number-field

Generate a Java field for an ACL2 quoted number.

Signature
(atj-gen-shallow-number-field number) → field
Arguments: number — Guard (acl2-numberp number).
Returns: field — Type (jfieldp field).

This is a private static final field with an initializer, which constructs the number value. The type and the initializer are the most specific applicable.

Definitions and Theorems

Function: atj-gen-shallow-number-field

(defun atj-gen-shallow-number-field (number)
  (declare (xargs :guard (acl2-numberp number)))
  (let ((__function__ 'atj-gen-shallow-number-field))
    (declare (ignorable __function__))
    (b* ((name (atj-gen-shallow-number-field-name number))
         (init (cond ((integerp number)
                      (atj-gen-integer number))
                     ((rationalp number)
                      (atj-gen-rational number))
                     (t (atj-gen-number number))))
         (type (cond ((integerp number) *aij-type-int*)
                     ((rationalp number) *aij-type-rational*)
                     (t *aij-type-number*))))
      (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-number-field

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