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