		Search-engine friendly clone of the ACL2 documentation.

Atj-java-primitive-array-model

Float-array-new-len

Construct a Java float array with the given length and with default components.

Signature
(float-array-new-len length) → array
Arguments: length — Guard (int-valuep length).
Returns: array — Type (float-arrayp array).

Definitions and Theorems

Function: float-array-new-len

(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: float-arrayp-of-float-array-new-len

(defthm float-arrayp-of-float-array-new-len
  (b* ((array (float-array-new-len length)))
    (float-arrayp array))
  :rule-classes :rewrite)