|
|
|---|
|
|
|
|---|
Raw constructor for honsed sd-key-p structures.
Syntax:
(honsed-sd-key pat index orig)
This is identical to sd-key, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by defaggregate.
Function:
(defun honsed-sd-key (pat index orig) (declare (xargs :guard (and (stringp pat) (maybe-natp index) (stringp orig)))) (mbe :logic (sd-key pat index orig) :exec (hons :sd-key (hons pat (hons index orig)))))