		Search-engine friendly clone of the ACL2 documentation.

S32v

S32v-resize-cols

Change the number of columns in the s32v, deleting data.

Logical definition:

Function: s32vl-resize-cols

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