|
|
|---|
|
|
|
|---|
Raw constructor for honsed constraint-rule-p structures.
Syntax:
(honsed-constraint-rule thmname lit-alist syntaxp)
This is identical to constraint-rule, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-constraint-rule (thmname lit-alist syntaxp) (declare (xargs :guard (and))) (mbe :logic (constraint-rule thmname lit-alist syntaxp) :exec (hons (hons 'thmname thmname) (hons (hons 'lit-alist lit-alist) (hons (hons 'syntaxp syntaxp) nil)))))