Basic constructor macro for svex-context-call structures.
(make-svex-context-call [:argnum <argnum>] [:fn <fn>] [:args <args>])
This is the usual way to construct svex-context-call structures. It simply conses together a structure with the specified fields.
This macro generates a new svex-context-call structure from scratch. See also change-svex-context-call, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-svex-context-call (&rest args) (std::make-aggregate 'svex-context-call args '((:argnum) (:fn) (:args)) 'make-svex-context-call nil))
Function:
(defun svex-context-call (argnum fn args) (declare (xargs :guard (and (natp argnum) (fnsym-p fn) (svexlist-p args)))) (declare (xargs :guard t)) (let ((__function__ 'svex-context-call)) (declare (ignorable __function__)) (b* ((argnum (mbe :logic (nfix argnum) :exec argnum)) (fn (mbe :logic (fnsym-fix fn) :exec fn)) (args (mbe :logic (svexlist-fix args) :exec args))) (cons :call (std::prod-cons argnum (std::prod-cons fn args))))))