		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-jshort

Generate Java code to build a Java short from a signed 16-bit signed ACL2 integer.

Signature
(atj-gen-jshort short) → expr
Arguments: short — Guard (sbyte16p short).
Returns: expr — Type (jexprp expr).

Definitions and Theorems

Function: atj-gen-jshort

(defun atj-gen-jshort (short)
  (declare (xargs :guard (sbyte16p short)))
  (let ((__function__ 'atj-gen-jshort))
    (declare (ignorable __function__))
    (jexpr-cast (jtype-short)
                (atj-gen-jint short))))

Theorem: jexprp-of-atj-gen-jshort

(defthm jexprp-of-atj-gen-jshort
  (b* ((expr (atj-gen-jshort short)))
    (jexprp expr))
  :rule-classes :rewrite)