|
|
|---|
|
|
|
|---|
Raw constructor for honsed wcp-template-p structures.
Syntax:
(honsed-wcp-template name enabledp
pat templ rulenames restriction)This is identical to wcp-template, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-wcp-template (name enabledp pat templ rulenames restriction) (declare (xargs :guard (and (symbolp name) (pseudo-termp pat) (pseudo-term-listp templ) (symbol-listp rulenames) (pseudo-termp restriction)))) (mbe :logic (wcp-template name enabledp pat templ rulenames restriction) :exec (hons (hons 'name name) (hons (hons 'enabledp enabledp) (hons (hons 'pat pat) (hons (hons 'templ templ) (hons (hons 'rulenames rulenames) (hons (hons 'restriction restriction) nil))))))))