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