		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-char-to-jhexcode

Turn an ACL2 character into a Java hexadecimal literal expression corresponding to the character code.

Signature
(atj-char-to-jhexcode char) → expr
Arguments: char — Guard (characterp char).
Returns: expr — Type (jexprp expr).

Definitions and Theorems

Function: atj-char-to-jhexcode

(defun atj-char-to-jhexcode (char)
 (declare (xargs :guard (characterp char)))
 (let ((__function__ 'atj-char-to-jhexcode))
  (declare (ignorable __function__))
  (b* ((code (char-code char))
       ((mv hi-char lo-char)
        (ubyte8=>hexchars code))
       (hi-code (char-code hi-char))
       (lo-code (char-code lo-char)))
   (jexpr-literal
    (jliteral-integer
      (integer-literal-hex
           (make-hex-integer-literal
                :digits/uscores (list (hexdig/uscore-digit hi-code)
                                      (hexdig/uscore-digit lo-code))
                :prefix-upcase-p nil
                :suffix? (optional-integer-type-suffix-none))))))))

Theorem: jexprp-of-atj-char-to-jhexcode

(defthm jexprp-of-atj-char-to-jhexcode
  (b* ((expr (atj-char-to-jhexcode char)))
    (jexprp expr))
  :rule-classes :rewrite)