		Search-engine friendly clone of the ACL2 documentation.

Vcd-wiremap

Set-vcdwire

Modify the nth element of the vcd-wiremap array.

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

Function: update-vcdwires$ai

(defun update-vcdwires$ai (stobjs::i stobjs::v vcd-wiremap$a)
  (declare (xargs :guard (and (vcd-wiremap$ap vcd-wiremap$a)
                              (integerp stobjs::i)
                              (<= 0 stobjs::i)
                              (< stobjs::i
                                 (vcdwires$a-length vcd-wiremap$a))
                              (vcd-wire-p stobjs::v)
                              (stobjs::typep$ stobjs::v t))))
  (ec-call (update-nth stobjs::i
                       (vcd-wire-fix$inline stobjs::v)
                       vcd-wiremap$a)))