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