Turn an ACL2 rational into a Java identifier part.
This is part of the names of the static final fields for quoted numbers.
If the rational is an integer,
we use atj-gen-shallow-integer-id-part.
Otherwise, we generate the integer numerator,
followed by
Function:
(defun atj-gen-shallow-rational-id-part (rational) (declare (xargs :guard (rationalp rational))) (let ((__function__ 'atj-gen-shallow-rational-id-part)) (declare (ignorable __function__)) (if (integerp rational) (atj-gen-shallow-integer-id-part rational) (str::cat (atj-gen-shallow-integer-id-part (numerator rational)) "_over_" (atj-gen-shallow-integer-id-part (denominator rational))))))
Theorem:
(defthm stringp-of-atj-gen-shallow-rational-id-part (b* ((core (atj-gen-shallow-rational-id-part rational))) (stringp core)) :rule-classes :rewrite)