(vl-scopeexpr->scopes x) → names
Function:
(defun vl-scopeexpr->scopes (x) (declare (xargs :guard (vl-expr-p x))) (declare (xargs :guard (vl-scopeexpr-p x))) (let ((__function__ 'vl-scopeexpr->scopes)) (declare (ignorable __function__)) (b* (((when (vl-atom-p x)) nil) ((vl-nonatom x) x) ((when (vl-op-equiv x.op :vl-scope)) (cons (vl-scopeatom->name (first x.args)) (vl-scopeexpr->scopes (second x.args))))) nil)))
Theorem:
(defthm vl-scopenamelist-p-of-vl-scopeexpr->scopes (b* ((names (vl-scopeexpr->scopes x))) (vl-scopenamelist-p names)) :rule-classes :rewrite)
Theorem:
(defthm vl-scopeexpr->scopes-of-vl-expr-fix-x (equal (vl-scopeexpr->scopes (vl-expr-fix x)) (vl-scopeexpr->scopes x)))
Theorem:
(defthm vl-scopeexpr->scopes-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-scopeexpr->scopes x) (vl-scopeexpr->scopes x-equiv))) :rule-classes :congruence)