		Search-engine friendly clone of the ACL2 documentation.

Atj-java-primitive-array-model

Double-array-read

Read a component from a Java double array.

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

Definitions and Theorems

Function: double-array-read

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

Theorem: double-valuep-of-double-array-read

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