		Search-engine friendly clone of the ACL2 documentation.

Atj-java-primitive-array-model

Float-array-read

Read a component from a Java float array.

Signature
(float-array-read array index) → component
Arguments: array — Guard (float-arrayp array).; index — Guard (int-valuep index).
Returns: component — Type (float-valuep component).

Definitions and Theorems

Function: float-array-read

(defun float-array-read (array index)
 (declare (xargs :guard (and (float-arrayp array)
                             (int-valuep index))))
 (declare (xargs :guard (float-array-index-in-range-p array index)))
 (let ((__function__ 'float-array-read))
   (declare (ignorable __function__))
   (float-value-fix (nth (int-value->int index)
                         (float-array->components array)))))

Theorem: float-valuep-of-float-array-read

(defthm float-valuep-of-float-array-read
  (b* ((component (float-array-read array index)))
    (float-valuep component))
  :rule-classes :rewrite)