|
|
|---|
|
|
|
|---|
Raw constructor for honsed prof-entry-p structures.
Syntax:
(honsed-prof-entry name tries-succ
tries-fail frames-succ frames-fail)This is identical to prof-entry, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-prof-entry (name tries-succ tries-fail frames-succ frames-fail) (declare (xargs :guard (and (natp tries-succ) (natp tries-fail) (natp frames-succ) (natp frames-fail)))) (mbe :logic (prof-entry name tries-succ tries-fail frames-succ frames-fail) :exec (hons (hons 'name name) (hons (hons 'tries-succ tries-succ) (hons (hons 'tries-fail tries-fail) (hons (hons 'frames-succ frames-succ) (hons (hons 'frames-fail frames-fail) nil)))))))