Construct a Java
(float-array-new-len length) → array
Function:
(defun float-array-new-len (length) (declare (xargs :guard (int-valuep length))) (declare (xargs :guard (>= (int-value->int length) 0))) (let ((__function__ 'float-array-new-len)) (declare (ignorable __function__)) (float-array (repeat (int-value->int length) (float-value (float-value-abs-pos-zero))))))
Theorem:
(defthm float-arrayp-of-float-array-new-len (b* ((array (float-array-new-len length))) (float-arrayp array)) :rule-classes :rewrite)