		Search-engine friendly clone of the ACL2 documentation.

Vcd-vector-p

Make-honsed-vcd-vector

Constructor macro for honsed vcd-vector-p structures.

Syntax:

(make-honsed-vcd-vector [:bits <bits>] 
                        [:idcode <idcode>])

This is identical to make-vcd-vector, except that we hons the structure we are creating.

Definition

This is an ordinary honsing make- macro introduced by defaggregate.

Macro: make-honsed-vcd-vector

(defmacro make-honsed-vcd-vector (&rest args)
  (std::make-aggregate 'vcd-vector
                       args '((:bits) (:idcode))
                       'make-honsed-vcd-vector
                       t))