		Search-engine friendly clone of the ACL2 documentation.

Array-operations

Value-array-read

Read an element from an array.

Signature
(value-array-read index array) → elem
Arguments: index — Guard (natp index).; array — Guard (valuep array).
Returns: elem — Type (value-resultp elem).

If the index is too large, it is an error.

Definitions and Theorems

Function: value-array-read

(defun value-array-read (index array)
  (declare (xargs :guard (and (natp index) (valuep array))))
  (declare (xargs :guard (value-case array :array)))
  (let ((__function__ 'value-array-read))
    (declare (ignorable __function__))
    (b* ((index (nfix index))
         ((unless (< index (value-array->length array)))
          (error (list :array-read-index
                       index (value-fix array)))))
      (nth index (value-array->elements array)))))

Theorem: value-resultp-of-value-array-read

(defthm value-resultp-of-value-array-read
  (b* ((elem (value-array-read index array)))
    (value-resultp elem))
  :rule-classes :rewrite)

Theorem: value-array-read-of-nfix-index

(defthm value-array-read-of-nfix-index
  (equal (value-array-read (nfix index) array)
         (value-array-read index array)))

Theorem: value-array-read-nat-equiv-congruence-on-index

(defthm value-array-read-nat-equiv-congruence-on-index
  (implies (acl2::nat-equiv index index-equiv)
           (equal (value-array-read index array)
                  (value-array-read index-equiv array)))
  :rule-classes :congruence)

Theorem: value-array-read-of-value-fix-array

(defthm value-array-read-of-value-fix-array
  (equal (value-array-read index (value-fix array))
         (value-array-read index array)))

Theorem: value-array-read-value-equiv-congruence-on-array

(defthm value-array-read-value-equiv-congruence-on-array
  (implies (value-equiv array array-equiv)
           (equal (value-array-read index array)
                  (value-array-read index array-equiv)))
  :rule-classes :congruence)