		Search-engine friendly clone of the ACL2 documentation.

S32v

S32v-resize-rows

Change the number of rows in the s32v, preserving data.

Logical definition:

Function: s32vl-resize-rows

(defun s32vl-resize-rows (stobjs::nrows s32vl-arr2)
 (declare
   (type (integer 0 *) stobjs::nrows)
   (xargs :guard (and (s32vl-arr2-wfp s32vl-arr2)
                      (<= stobjs::nrows (1- (expt 2 60)))
                      (<= (* stobjs::nrows (s32vl-ncols s32vl-arr2))
                          (1- (expt 2 60))))))
 (stobjs::2darr (stobjs::2darr->ncols s32vl-arr2)
                (resize-list (stobjs::2darr->rows s32vl-arr2)
                             (nfix stobjs::nrows)
                             (make-list (s32vl-ncols s32vl-arr2)
                                        :initial-element 0))))