(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 (vl-expr-fix expr) (vl-datatype-allexprs (vl-vardecl->type elem))) t nil)) (:vl-paramdecl t) (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)
Theorem:
(defthm vl-expr-indexy-via-ctx-of-vl-expr-fix-expr (equal (vl-expr-indexy-via-ctx (vl-expr-fix expr) ctx) (vl-expr-indexy-via-ctx expr ctx)))
Theorem:
(defthm vl-expr-indexy-via-ctx-vl-expr-equiv-congruence-on-expr (implies (vl-expr-equiv expr expr-equiv) (equal (vl-expr-indexy-via-ctx expr ctx) (vl-expr-indexy-via-ctx expr-equiv ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-expr-indexy-via-ctx-of-vl-context1-fix-ctx (equal (vl-expr-indexy-via-ctx expr (vl-context1-fix ctx)) (vl-expr-indexy-via-ctx expr ctx)))
Theorem:
(defthm vl-expr-indexy-via-ctx-vl-context1-equiv-congruence-on-ctx (implies (vl-context1-equiv ctx ctx-equiv) (equal (vl-expr-indexy-via-ctx expr ctx) (vl-expr-indexy-via-ctx expr ctx-equiv))) :rule-classes :congruence)