|
|
|---|
|
|
|
|---|
Raw constructor for wcp-instance-rule-p structures.
Syntax:
(wcp-instance-rule name enabledp
pred vars expr restriction theorem)This is the lowest-level constructor for wcp-instance-rule-p structures. It simply conses together a structure with the specified fields.
Note: It's generally better to use macros like make-wcp-instance-rule or change-wcp-instance-rule instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.
The wcp-instance-rule-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-wcp-instance-rule instead.
This is an ordinary constructor function introduced by std::defaggregate.
Function:
(defun wcp-instance-rule (name enabledp pred vars expr restriction theorem) (declare (xargs :guard (and (symbolp name) (pseudo-termp pred) (and (symbol-listp vars) (not (intersectp-equal vars (simple-term-vars pred)))) (pseudo-termp expr) (pseudo-termp restriction) (symbolp theorem)))) (cons (cons 'name name) (cons (cons 'enabledp enabledp) (cons (cons 'pred pred) (cons (cons 'vars vars) (cons (cons 'expr expr) (cons (cons 'restriction restriction) (cons (cons 'theorem theorem) nil))))))))