|
|
|---|
|
|
|
|---|
Raw constructor for wcp-template-p structures.
Syntax:
(wcp-template name enabledp
pat templ rulenames restriction)This is the lowest-level constructor for wcp-template-p structures. It simply conses together a structure with the specified fields.
Note: It's generally better to use macros like make-wcp-template or change-wcp-template instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.
The wcp-template-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-wcp-template instead.
This is an ordinary constructor function introduced by std::defaggregate.
Function:
(defun 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)))) (cons (cons 'name name) (cons (cons 'enabledp enabledp) (cons (cons 'pat pat) (cons (cons 'templ templ) (cons (cons 'rulenames rulenames) (cons (cons 'restriction restriction) nil)))))))