Raw constructor for honsed vl-dupeinst-key-p structures.
Syntax:
(honsed-vl-dupeinst-key modname inputs)
Since vl-dupeinst-key-p structures are always honsed, this is identical to vl-dupeinst-key. We introduce it mainly for consistency with other defaggregate style structures.
This is an ordinary honsing constructor introduced by defaggregate.
Function:
(defun honsed-vl-dupeinst-key (modname inputs) (declare (xargs :guard (and (stringp modname) (vl-exprlist-p inputs)))) (mbe :logic (vl-dupeinst-key modname inputs) :exec (hons :vl-dupeinst-key (hons (hons 'modname modname) (hons (hons 'inputs inputs) nil)))))