|
|
|---|
|
|
|
|---|
Raw constructor for honsed wcp-instance-rule-p structures.
Syntax:
(honsed-wcp-instance-rule name enabledp
pred vars expr restriction theorem)This is identical to wcp-instance-rule, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-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)))) (mbe :logic (wcp-instance-rule name enabledp pred vars expr restriction theorem) :exec (hons (hons 'name name) (hons (hons 'enabledp enabledp) (hons (hons 'pred pred) (hons (hons 'vars vars) (hons (hons 'expr expr) (hons (hons 'restriction restriction) (hons (hons 'theorem theorem) nil)))))))))