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