(vl-pps-scopestack-path x) → str
Function:
(defun vl-pps-scopestack-path (x) (declare (xargs :guard (vl-scopestack-p x))) (let ((__function__ 'vl-pps-scopestack-path)) (declare (ignorable __function__)) (with-local-ps (vl-pp-scopestack-path x))))
Theorem:
(defthm stringp-of-vl-pps-scopestack-path (b* ((str (vl-pps-scopestack-path x))) (stringp str)) :rule-classes :type-prescription)
Theorem:
(defthm vl-pps-scopestack-path-of-vl-scopestack-fix-x (equal (vl-pps-scopestack-path (vl-scopestack-fix x)) (vl-pps-scopestack-path x)))
Theorem:
(defthm vl-pps-scopestack-path-vl-scopestack-equiv-congruence-on-x (implies (vl-scopestack-equiv x x-equiv) (equal (vl-pps-scopestack-path x) (vl-pps-scopestack-path x-equiv))) :rule-classes :congruence)