Generate the name of the Java field for an ACL2 quoted string.
We prepend
Function:
(defun atj-gen-shallow-string-field-name (string) (declare (xargs :guard (stringp string))) (let ((__function__ 'atj-gen-shallow-string-field-name)) (declare (ignorable __function__)) (str::cat "$S_" (implode (atj-chars-to-jchars-id (explode string) nil :space nil)))))
Theorem:
(defthm stringp-of-atj-gen-shallow-string-field-name (b* ((name (atj-gen-shallow-string-field-name string))) (stringp name)) :rule-classes :rewrite)