(vl-expr-indexy-via-ctx expr ctx) → indexy
Function:
(defun vl-expr-indexy-via-ctx (expr ctx) (declare (xargs :guard (and (vl-expr-p expr) (vl-context1-p ctx)))) (let ((__function__ 'vl-expr-indexy-via-ctx)) (declare (ignorable __function__)) (b* ((elem (vl-context1->elem ctx))) (case (tag elem) (:vl-vardecl (if (member-equal expr (vl-datatype-allexprs (vl-vardecl->type elem))) t nil)) (otherwise nil)))))
Theorem:
(defthm booleanp-of-vl-expr-indexy-via-ctx (b* ((indexy (vl-expr-indexy-via-ctx expr ctx))) (booleanp indexy)) :rule-classes :type-prescription)