		Search-engine friendly clone of the ACL2 documentation.

S32v

S32v-set2

Set the element at arr[row][col] in the s32v array to some new value.

Logical definition:

Function: s32vl-set2

(defun s32vl-set2 (stobjs::row stobjs::col stobjs::val s32vl-arr2)
 (declare
      (type (integer 0 *) stobjs::row)
      (type (integer 0 *) stobjs::col)
      (type (signed-byte 32) stobjs::val)
      (xargs :guard (and (s32vl-arr2-wfp s32vl-arr2)
                         (< stobjs::row (s32vl-nrows s32vl-arr2))
                         (< stobjs::col (s32vl-ncols s32vl-arr2)))))
 (stobjs::2darr
     (stobjs::2darr->ncols s32vl-arr2)
     (update-nth stobjs::row
                 (update-nth stobjs::col stobjs::val
                             (nth stobjs::row
                                  (stobjs::2darr->rows s32vl-arr2)))
                 (stobjs::2darr->rows s32vl-arr2))))