Raw constructor for honsed wcp-example-app-p structures.
Syntax:
(honsed-wcp-example-app instrule bindings)
This is identical to wcp-example-app, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-wcp-example-app (instrule bindings) (declare (xargs :guard (and (wcp-instance-rule-p instrule) (and (pseudo-term-listp bindings) (eql (len bindings) (len (wcp-instance-rule->vars instrule))))))) (mbe :logic (wcp-example-app instrule bindings) :exec (hons (hons 'instrule instrule) (hons (hons 'bindings bindings) nil))))