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