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