		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.