|
|
|---|
|
|
|
|---|
Raw constructor for honsed defarbrec-infop structures.
Syntax:
(honsed-defarbrec-info call$ expansion x1...xn body
update-fns terminates-fn measure-fn)This is identical to defarbrec-info, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-defarbrec-info (call$ expansion x1...xn body update-fns terminates-fn measure-fn) (declare (xargs :guard (and (pseudo-event-formp call$) (pseudo-event-formp expansion) (symbol-listp update-fns) (symbolp terminates-fn) (symbolp measure-fn)))) (mbe :logic (defarbrec-info call$ expansion x1...xn body update-fns terminates-fn measure-fn) :exec (hons (hons 'call$ call$) (hons (hons 'expansion expansion) (hons (hons 'x1...xn x1...xn) (hons (hons 'body body) (hons (hons 'update-fns update-fns) (hons (hons 'terminates-fn terminates-fn) (hons (hons 'measure-fn measure-fn) nil)))))))))