Turn an ACL2 integer into a Java identifier part.
This is part of the names of the static final fields for quoted numbers.
We turn the integer into its (base 10) digits,
prepended by
Function:
(defun atj-gen-shallow-integer-id-part (integer) (declare (xargs :guard (integerp integer))) (let ((__function__ 'atj-gen-shallow-integer-id-part)) (declare (ignorable __function__)) (if (>= integer 0) (nat-to-dec-string integer) (str::cat "minus" (nat-to-dec-string (- integer))))))
Theorem:
(defthm stringp-of-atj-gen-shallow-integer-id-part (b* ((core (atj-gen-shallow-integer-id-part integer))) (stringp core)) :rule-classes :rewrite)