		Search-engine friendly clone of the ACL2 documentation.

Bitarr

Set-bit

Modify the nth element of the bitarr array.

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

Function: update-bits$ai

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