Raw constructor for honsed vl-udp-body-p structures.
Syntax:
(honsed-vl-udp-body init table)
This is identical to vl-udp-body, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by defaggregate.
Function:
(defun honsed-vl-udp-body (init table) (declare (xargs :guard (and (vl-maybe-expr-p init) (vl-udptable-p table)))) (mbe :logic (vl-udp-body init table) :exec (hons init table)))