		Search-engine friendly clone of the ACL2 documentation.

S32v

S32v-get2

Get the element at arr[row][col] from the s32v array.

Logical definition:

Function: s32vl-get2

(defun s32vl-get2 (stobjs::row stobjs::col s32vl-arr2)
 (declare
      (type (integer 0 *) stobjs::row)
      (type (integer 0 *) stobjs::col)
      (xargs :guard (and (s32vl-arr2-wfp s32vl-arr2)
                         (< stobjs::row (s32vl-nrows s32vl-arr2))
                         (< stobjs::col (s32vl-ncols s32vl-arr2)))))
 (s32-fix (nth stobjs::col
               (nth stobjs::row
                    (stobjs::2darr->rows s32vl-arr2)))))