		Search-engine friendly clone of the ACL2 documentation.

Bitarr

Get-bit

Read the nth element of the bitarr array.

In the execution this is an array access, but the logical definition is just a thin wrapper for nth:

Function: bits$ai

(defun
   bits$ai (stobjs::i bitarr$a)
   (declare
        (xargs :guard (and (bitarr$ap bitarr$a)
                           (integerp stobjs::i)
                           (<= 0 stobjs::i)
                           (< stobjs::i (bits$a-length bitarr$a)))))
   (ec-call (bfix (ec-call (nth stobjs::i bitarr$a)))))