|
|
|---|
|
|
|
|---|
Raw constructor for honsed vcd-vector-p structures.
Syntax:
(honsed-vcd-vector bits idcode)
This is identical to vcd-vector, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by defaggregate.
Function:
(defun honsed-vcd-vector (bits idcode) (declare (xargs :guard (and (stringp idcode)))) (mbe :logic (vcd-vector bits idcode) :exec (hons :vcd-vector (hons bits idcode))))