Read an element from an array of type
(sint-array-read array index) → element
Function:
(defun sint-array-read (array index) (declare (xargs :guard (and (sint-arrayp array) (cintegerp index)))) (declare (xargs :guard (sint-array-index-okp array index))) (let ((__function__ 'sint-array-read)) (declare (ignorable __function__)) (sint-fix (nth (integer-from-cinteger index) (sint-array->elements array)))))
Theorem:
(defthm sintp-of-sint-array-read (b* ((element (sint-array-read array index))) (sintp element)) :rule-classes :rewrite)
Theorem:
(defthm sint-array-read-alt-def (implies (and (sint-arrayp array) (cintegerp index) (sint-array-index-okp array index)) (equal (sint-array-read array index) (value-array-read (integer-from-cinteger index) array))))
Theorem:
(defthm sint-array-read-of-sint-array-fix-array (equal (sint-array-read (sint-array-fix array) index) (sint-array-read array index)))
Theorem:
(defthm sint-array-read-sint-array-equiv-congruence-on-array (implies (sint-array-equiv array array-equiv) (equal (sint-array-read array index) (sint-array-read array-equiv index))) :rule-classes :congruence)
Theorem:
(defthm sint-array-read-of-cinteger-fix-index (equal (sint-array-read array (cinteger-fix index)) (sint-array-read array index)))
Theorem:
(defthm sint-array-read-cinteger-equiv-congruence-on-index (implies (cinteger-equiv index index-equiv) (equal (sint-array-read array index) (sint-array-read array index-equiv))) :rule-classes :congruence)