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