		Search-engine friendly clone of the ACL2 documentation.

Frames

Frames-set2

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

Logical definition:

Function: framesl-set2

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