		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-jbigint

Generate Java code to build a Java BigInteger from an ACL2 integer.

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

Definitions and Theorems

Function: atj-gen-jbigint

(defun atj-gen-jbigint (integer)
  (declare (xargs :guard (integerp integer)))
  (let ((__function__ 'atj-gen-jbigint))
    (declare (ignorable __function__))
    (b* ((string (if (< integer 0)
                     (str::cat "-" (nat-to-dec-string (- integer)))
                   (nat-to-dec-string integer))))
      (jexpr-newclass (jtype-class "BigInteger")
                      (list (jexpr-literal-string string))))))

Theorem: jexprp-of-atj-gen-jbigint

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