Construct a Java
(double-array-new-init comps) → array
Function:
(defun double-array-new-init (comps) (declare (xargs :guard (double-value-listp comps))) (declare (xargs :guard (< (len comps) (expt 2 31)))) (let ((__function__ 'double-array-new-init)) (declare (ignorable __function__)) (double-array comps)))
Theorem:
(defthm double-arrayp-of-double-array-new-init (b* ((array (double-array-new-init comps))) (double-arrayp array)) :rule-classes :rewrite)