|
|
|---|
|
|
|
|---|
Raw constructor for honsed boundrw-subst-p structures.
Syntax:
(honsed-boundrw-subst lhs rhs alist)
This is identical to boundrw-subst, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-boundrw-subst (lhs rhs alist) (declare (xargs :guard (and (pseudo-termp lhs) (pseudo-termp rhs) (pseudo-term-substp alist)))) (mbe :logic (boundrw-subst lhs rhs alist) :exec (hons (hons 'lhs lhs) (hons (hons 'rhs rhs) (hons (hons 'alist alist) nil)))))