Turn an ACL2 number into a Java identifier part.
(atj-gen-shallow-number-id-part number) → 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
Function:
(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:
(defthm stringp-of-atj-gen-shallow-number-id-part (b* ((core (atj-gen-shallow-number-id-part number))) (stringp core)) :rule-classes :rewrite)