Generate the name of the Java field for an ACL2 quoted number.
(atj-gen-shallow-number-field-name number) → name
We prepend
Function:
(defun atj-gen-shallow-number-field-name (number) (declare (xargs :guard (acl2-numberp number))) (let ((__function__ 'atj-gen-shallow-number-field-name)) (declare (ignorable __function__)) (str::cat "$N_" (atj-gen-shallow-number-id-part number))))
Theorem:
(defthm stringp-of-atj-gen-shallow-number-field-name (b* ((name (atj-gen-shallow-number-field-name number))) (stringp name)) :rule-classes :rewrite)