		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-jlong

Generate Java code to build a Java long from a signed 64-bit ACL2 integer.

Signature
(atj-gen-jlong integer) → expr
Arguments: integer — Guard (sbyte64p integer).
Returns: expr — Type (jexprp expr).

Definitions and Theorems

Function: atj-gen-jlong

(defun atj-gen-jlong (integer)
  (declare (xargs :guard (sbyte64p integer)))
  (let ((__function__ 'atj-gen-jlong))
    (declare (ignorable __function__))
    (if (< integer 0)
        (jexpr-unary (junop-uminus)
                     (jexpr-lit-long-dec-nouscores (- integer)))
      (jexpr-lit-long-dec-nouscores integer))))

Theorem: jexprp-of-atj-gen-jlong

(defthm jexprp-of-atj-gen-jlong
  (b* ((expr (atj-gen-jlong integer)))
    (jexprp expr))
  :rule-classes :rewrite)