		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-number-id-part

Turn an ACL2 number into a Java identifier part.

Signature
(atj-gen-shallow-number-id-part number) → core
Arguments: number — Guard (acl2-numberp number).
Returns: core — Type (stringp core).

This is part of the names of the static final fields for quoted numbers.

If the number is a rational, we use atj-gen-shallow-rational-id-part. Otherwise, we generate the rational real part, followed by _plus_i_ to denote the formal complex sum, followed by the rational imaginary part (never 0).

Definitions and Theorems

Function: atj-gen-shallow-number-id-part

(defun atj-gen-shallow-number-id-part (number)
  (declare (xargs :guard (acl2-numberp number)))
  (let ((__function__ 'atj-gen-shallow-number-id-part))
    (declare (ignorable __function__))
    (if (rationalp number)
        (atj-gen-shallow-rational-id-part number)
      (str::cat
           (atj-gen-shallow-rational-id-part (realpart number))
           "_plus_i_"
           (atj-gen-shallow-rational-id-part (imagpart number))))))

Theorem: stringp-of-atj-gen-shallow-number-id-part

(defthm stringp-of-atj-gen-shallow-number-id-part
  (b* ((core (atj-gen-shallow-number-id-part number)))
    (stringp core))
  :rule-classes :rewrite)