|
|
|---|
|
|
|
|---|
Raw constructor for wcp-witness-rule-p structures.
Syntax:
(wcp-witness-rule name enabledp term
expr restriction theorem generalize)This is the lowest-level constructor for wcp-witness-rule-p structures. It simply conses together a structure with the specified fields.
Note: It's generally better to use macros like make-wcp-witness-rule or change-wcp-witness-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-witness-rule-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-wcp-witness-rule instead.
This is an ordinary constructor function introduced by std::defaggregate.
Function:
(defun wcp-witness-rule (name enabledp term expr restriction theorem generalize) (declare (xargs :guard (and (symbolp name) (pseudo-termp term) (pseudo-termp expr) (symbolp theorem) (and (alistp generalize) (pseudo-term-listp (strip-cars generalize)) (symbol-listp (strip-cdrs generalize)))))) (cons (cons 'name name) (cons (cons 'enabledp enabledp) (cons (cons 'term term) (cons (cons 'expr expr) (cons (cons 'restriction restriction) (cons (cons 'theorem theorem) (cons (cons 'generalize generalize) nil))))))))