		Search-engine friendly clone of the ACL2 documentation.

Frames

Frames-get2

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

Logical definition:

Function: framesl-get2

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