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