|
|
|---|
|
|
|
|---|
Raw constructor for defarbrec-infop structures.
Syntax:
(defarbrec-info call$ expansion x1...xn body
update-fns terminates-fn measure-fn)This is the lowest-level constructor for defarbrec-infop structures. It simply conses together a structure with the specified fields.
Note: It's generally better to use macros like make-defarbrec-info or change-defarbrec-info instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.
The defarbrec-infop structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-defarbrec-info instead.
This is an ordinary constructor function introduced by std::defaggregate.
Function:
(defun 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)))) (cons (cons 'call$ call$) (cons (cons 'expansion expansion) (cons (cons 'x1...xn x1...xn) (cons (cons 'body body) (cons (cons 'update-fns update-fns) (cons (cons 'terminates-fn terminates-fn) (cons (cons 'measure-fn measure-fn) nil))))))))