(vl-scopeatom->name x) → name
Function:
(defun vl-scopeatom->name (x) (declare (xargs :guard (vl-expr-p x))) (declare (xargs :guard (vl-scopeatom-p x))) (let ((__function__ 'vl-scopeatom->name)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x))) (if (vl-hidname-p x) (vl-hidname->name x) (vl-scopename-fix (vl-keyguts->type (vl-atom->guts x)))))))
Theorem:
(defthm vl-scopename-p-of-vl-scopeatom->name (b* ((name (vl-scopeatom->name x))) (vl-scopename-p name)) :rule-classes :rewrite)
Theorem:
(defthm vl-scopeatom->name-of-vl-expr-fix-x (equal (vl-scopeatom->name (vl-expr-fix x)) (vl-scopeatom->name x)))
Theorem:
(defthm vl-scopeatom->name-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-scopeatom->name x) (vl-scopeatom->name x-equiv))) :rule-classes :congruence)