		Search-engine friendly clone of the ACL2 documentation.

Std/stobjs

Bitarr

Abstract stobj: logically this just represents a list of |ACL2|::|BITP|s, but it is implemented as an array.

This is a simple abstract stobj array, introduced by def-1d-arr.

Definition: bitarr

(defabsstobj bitarr
  :foundation bitarr$c
  :recognizer (bitarrp :exec bitarr$cp
                       :logic bitarr$ap)
  :creator (create-bitarr :exec create-bitarr$c
                          :logic create-bitarr$a)
  :corr-fn bitarr$corr
  :exports ((bits-length :exec bits$c-length
                         :logic bits$a-length)
            (get-bit :exec bits$ci :logic bits$ai)
            (set-bit :exec update-bits$ci
                     :logic update-bits$ai)
            (resize-bits :exec resize-bits$c
                         :logic resize-bits$a)))

Subtopics

Bits-equiv: Bit-for-bit list equivalence: bits-equiv recognizes lists whose nth elements are bit-equiv to one another. It is often useful for reasoning about bit arrays like bitarr.
Set-bit: Modify the nth element of the bitarr array.
Resize-bits: Change the length of the bitarr array.
Get-bit: Read the nth element of the bitarr array.
Bits-length: Get the length of the bitarr array.