		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-jbyte

Generate Java code to build a Java byte from a signed 8-bit ACL2 integer.

Signature
(atj-gen-jbyte byte) → expr
Arguments: byte — Guard (sbyte8p byte).
Returns: expr — Type (jexprp expr).

Definitions and Theorems

Function: atj-gen-jbyte

(defun atj-gen-jbyte (byte)
  (declare (xargs :guard (sbyte8p byte)))
  (let ((__function__ 'atj-gen-jbyte))
    (declare (ignorable __function__))
    (jexpr-cast (jtype-byte)
                (atj-gen-jint byte))))

Theorem: jexprp-of-atj-gen-jbyte

(defthm jexprp-of-atj-gen-jbyte
  (b* ((expr (atj-gen-jbyte byte)))
    (jexprp expr))
  :rule-classes :rewrite)