Generate a shallowly embedded ACL2 quoted character.
(atj-gen-shallow-char char guards$) → expr
If guards are assumed, we generate the corresponding Java character literal.
Otherwise, we generate a reference to the field for the quoted character.
Function:
(defun atj-gen-shallow-char (char guards$) (declare (xargs :guard (and (characterp char) (booleanp guards$)))) (let ((__function__ 'atj-gen-shallow-char)) (declare (ignorable __function__)) (if guards$ (jexpr-literal-character char) (jexpr-name (atj-gen-shallow-char-field-name char)))))
Theorem:
(defthm jexprp-of-atj-gen-shallow-char (b* ((expr (atj-gen-shallow-char char guards$))) (jexprp expr)) :rule-classes :rewrite)