		Search-engine friendly clone of the ACL2 documentation.

Ubdd-arr

Set-ubdd

Modify the nth element of the ubdd-arr array.

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

Function: update-ubdds$ai

(defun update-ubdds$ai (stobjs::i stobjs::v ubdd-arr$a)
  (declare
       (xargs :guard (and (ubdd-arr$ap ubdd-arr$a)
                          (integerp stobjs::i)
                          (<= 0 stobjs::i)
                          (< stobjs::i (ubdds$a-length ubdd-arr$a))
                          (acl2::ubddp stobjs::v)
                          (stobjs::typep$ stobjs::v t))))
  (ec-call (update-nth stobjs::i (acl2::ubdd-fix stobjs::v)
                       ubdd-arr$a)))