|
|
|---|
|
|
|
|---|
Raw constructor for honsed atc-call-infop structures.
Syntax:
(honsed-atc-call-info encapsulate)
This is identical to atc-call-info, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-atc-call-info (encapsulate) (declare (xargs :guard (and (pseudo-event-formp encapsulate)))) (mbe :logic (atc-call-info encapsulate) :exec (hons (hons 'encapsulate encapsulate) nil)))