Promote an vl-scopeexpr into a proper vl-index without any part select.
(vl-scopeexpr->expr x) → expr
Function:
(defun vl-scopeexpr->expr (x) (declare (xargs :guard (vl-scopeexpr-p x))) (let ((__function__ 'vl-scopeexpr->expr)) (declare (ignorable __function__)) (make-vl-index :scope x :indices nil :part (make-vl-partselect-none) :atts nil)))
Theorem:
(defthm vl-expr-p-of-vl-scopeexpr->expr (b* ((expr (vl-scopeexpr->expr x))) (vl-expr-p expr)) :rule-classes :rewrite)
Theorem:
(defthm vl-scopeexpr->expr-of-vl-scopeexpr-fix-x (equal (vl-scopeexpr->expr (vl-scopeexpr-fix x)) (vl-scopeexpr->expr x)))
Theorem:
(defthm vl-scopeexpr->expr-vl-scopeexpr-equiv-congruence-on-x (implies (vl-scopeexpr-equiv x x-equiv) (equal (vl-scopeexpr->expr x) (vl-scopeexpr->expr x-equiv))) :rule-classes :congruence)