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