		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-char

Generate a shallowly embedded ACL2 quoted character.

Signature
(atj-gen-shallow-char char guards$) → expr
Arguments: char — Guard (characterp char).; guards$ — Guard (booleanp guards$).
Returns: expr — Type (jexprp expr).

If guards are assumed, we generate the corresponding Java character literal.

Otherwise, we generate a reference to the field for the quoted character.

Definitions and Theorems

Function: atj-gen-shallow-char

(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: jexprp-of-atj-gen-shallow-char

(defthm jexprp-of-atj-gen-shallow-char
  (b* ((expr (atj-gen-shallow-char char guards$)))
    (jexprp expr))
  :rule-classes :rewrite)