Generate Java code to build a Java
(atj-gen-jint-array int-array) → expr
Function:
(defun atj-gen-jint-array-aux (ints) (declare (xargs :guard (int-value-listp ints))) (let ((__function__ 'atj-gen-jint-array-aux)) (declare (ignorable __function__)) (cond ((endp ints) nil) (t (cons (atj-gen-jint (int-value->int (car ints))) (atj-gen-jint-array-aux (cdr ints)))))))
Theorem:
(defthm jexpr-listp-of-atj-gen-jint-array-aux (b* ((exprs (atj-gen-jint-array-aux ints))) (jexpr-listp exprs)) :rule-classes :rewrite)
Function:
(defun atj-gen-jint-array (int-array) (declare (xargs :guard (int-arrayp int-array))) (let ((__function__ 'atj-gen-jint-array)) (declare (ignorable __function__)) (jexpr-newarray-init (jtype-int) (atj-gen-jint-array-aux (int-array->components int-array)))))
Theorem:
(defthm jexprp-of-atj-gen-jint-array (b* ((expr (atj-gen-jint-array int-array))) (jexprp expr)) :rule-classes :rewrite)