Basic constructor macro for eval-state-init structures.
(make-eval-state-init [:function <function>] [:arguments <arguments>])
This is the usual way to construct eval-state-init structures. It simply conses together a structure with the specified fields.
This macro generates a new eval-state-init structure from scratch. See also change-eval-state-init, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-eval-state-init (&rest args) (std::make-aggregate 'eval-state-init args '((:function) (:arguments)) 'make-eval-state-init nil))
Function:
(defun eval-state-init (function arguments) (declare (xargs :guard (and (symbol-valuep function) (value-listp arguments)))) (declare (xargs :guard t)) (let ((__function__ 'eval-state-init)) (declare (ignorable __function__)) (b* ((function (mbe :logic (symbol-value-fix function) :exec function)) (arguments (mbe :logic (value-list-fix arguments) :exec arguments))) (cons :init (list function arguments)))))