		Search-engine friendly clone of the ACL2 documentation.

Atc-arrays

Sshort-array-read

Read an element from an array of type signed short, using a C integer index.

Signature
(sshort-array-read array index) → element
Arguments: array — Guard (sshort-arrayp array).; index — Guard (cintegerp index).
Returns: element — Type (sshortp element).

Definitions and Theorems

Function: sshort-array-read

(defun sshort-array-read (array index)
  (declare (xargs :guard (and (sshort-arrayp array)
                              (cintegerp index))))
  (declare (xargs :guard (sshort-array-index-okp array index)))
  (let ((__function__ 'sshort-array-read))
    (declare (ignorable __function__))
    (sshort-fix (nth (integer-from-cinteger index)
                     (sshort-array->elements array)))))

Theorem: sshortp-of-sshort-array-read

(defthm sshortp-of-sshort-array-read
  (b* ((element (sshort-array-read array index)))
    (sshortp element))
  :rule-classes :rewrite)

Theorem: sshort-array-read-alt-def

(defthm sshort-array-read-alt-def
  (implies (and (sshort-arrayp array)
                (cintegerp index)
                (sshort-array-index-okp array index))
           (equal (sshort-array-read array index)
                  (value-array-read (integer-from-cinteger index)
                                    array))))

Theorem: sshort-array-read-of-sshort-array-fix-array

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

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

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

Theorem: sshort-array-read-of-cinteger-fix-index

(defthm sshort-array-read-of-cinteger-fix-index
  (equal (sshort-array-read array (cinteger-fix index))
         (sshort-array-read array index)))

Theorem: sshort-array-read-cinteger-equiv-congruence-on-index

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