		Search-engine friendly clone of the ACL2 documentation.

Undocumented

Frames

Abstract stobj that implements a two dimensional array of bitps.

This is a two dimensional abstract stobj array, introduced by def-2d-arr.

Definition: frames

(defabsstobj frames
  :foundation framese-arr2
  :recognizer (framesp :logic framesl-arr2-wfp
                       :exec framese-arr2p)
  :creator (create-frames :logic create-framesl-arr2
                          :exec create-framese-arr2)
  :corr-fn frames-corr
  :exports ((frames-nrows :logic framesl-nrows
                          :exec framese-nrows)
            (frames-ncols :logic framesl-ncols
                          :exec framese-ncols)
            (frames-get2 :logic framesl-get2
                         :exec framese-get2$inline)
            (frames-get :logic framesl-get
                        :exec framese-get$inline)
            (frames-set2$g :logic framesl-set2
                           :exec framese-set2$inline)
            (frames-set$g :logic framesl-set
                          :exec framese-set$inline)
            (frames-resize-rows$g :logic framesl-resize-rows
                                  :exec framese-resize-rows$inline
                                  :protect t)
            (frames-resize-cols$g :logic framesl-resize-cols
                                  :exec framese-resize-cols$inline
                                  :protect t)))

Definition: frames

(defabsstobj frames
  :foundation framese-arr2
  :recognizer (framesp :logic framesl-arr2-wfp
                       :exec framese-arr2p)
  :creator (create-frames :logic create-framesl-arr2
                          :exec create-framese-arr2)
  :corr-fn frames-corr
  :exports ((frames-nrows :logic framesl-nrows
                          :exec framese-nrows)
            (frames-ncols :logic framesl-ncols
                          :exec framese-ncols)
            (frames-get2 :logic framesl-get2
                         :exec framese-get2$inline)
            (frames-get :logic framesl-get
                        :exec framese-get$inline)
            (frames-set2$g :logic framesl-set2
                           :exec framese-set2$inline)
            (frames-set$g :logic framesl-set
                          :exec framese-set$inline)
            (frames-resize-rows$g :logic framesl-resize-rows
                                  :exec framese-resize-rows$inline
                                  :protect t)
            (frames-resize-cols$g :logic framesl-resize-cols
                                  :exec framese-resize-cols$inline
                                  :protect t)))

Subtopics

Frames-set2: Set the element at arr[row][col] in the frames array to some new value.
Frames-resize-rows: Change the number of rows in the frames, preserving data.
Frames-resize-cols: Change the number of columns in the frames, deleting data.
Frames-get2: Get the element at arr[row][col] from the frames array.
Frames-nrows: Get the number of rows in the frames array.
Frames-ncols: Get the number of columns in the frames array.