		Search-engine friendly clone of the ACL2 documentation.

Vcd-wiremap

Get-vcdwire

Read the nth element of the vcd-wiremap array.

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

Function: vcdwires$ai

(defun vcdwires$ai (stobjs::i 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)))))
 (ec-call
     (vcd-wire-fix$inline (ec-call (nth stobjs::i vcd-wiremap$a)))))