		Search-engine friendly clone of the ACL2 documentation.

Obs-sdom-array

Set-sdominfo

Modify the nth element of the obs-sdom-array array.

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

Function: update-sdominfos$ai

(defun update-sdominfos$ai (stobjs::i stobjs::v obs-sdom-array$a)
  (declare
       (xargs :guard (and (obs-sdom-array$ap obs-sdom-array$a)
                          (integerp stobjs::i)
                          (<= 0 stobjs::i)
                          (< stobjs::i
                             (sdominfos$a-length obs-sdom-array$a))
                          (obs-sdom-info-p stobjs::v)
                          (stobjs::typep$ stobjs::v t))))
  (ec-call (update-nth stobjs::i (obs-sdom-info-fix stobjs::v)
                       obs-sdom-array$a)))