(vl-scopestack-find-elabpath ss context-ss pkg-name) → elabpath
Function:
(defun vl-scopestack-find-elabpath (ss context-ss pkg-name) (declare (xargs :guard (and (vl-scopestack-p ss) (vl-scopestack-p context-ss) (maybe-stringp pkg-name)))) (declare (xargs :guard (<= (vl-scopestack-nesting-level context-ss) (vl-scopestack-nesting-level ss)))) (let ((__function__ 'vl-scopestack-find-elabpath)) (declare (ignorable __function__)) (if pkg-name (list (vl-elabinstruction-push-named (vl-elabkey-package pkg-name)) (vl-elabinstruction-root)) (b* ((levels-up (- (vl-scopestack-nesting-level ss) (vl-scopestack-nesting-level context-ss)))) (list (vl-elabinstruction-pop levels-up))))))
Theorem:
(defthm vl-elabtraversal-p-of-vl-scopestack-find-elabpath (b* ((elabpath (vl-scopestack-find-elabpath ss context-ss pkg-name))) (vl-elabtraversal-p elabpath)) :rule-classes :rewrite)
Theorem:
(defthm vl-scopestack-find-elabpath-of-vl-scopestack-fix-ss (equal (vl-scopestack-find-elabpath (vl-scopestack-fix ss) context-ss pkg-name) (vl-scopestack-find-elabpath ss context-ss pkg-name)))
Theorem:
(defthm vl-scopestack-find-elabpath-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-scopestack-find-elabpath ss context-ss pkg-name) (vl-scopestack-find-elabpath ss-equiv context-ss pkg-name))) :rule-classes :congruence)
Theorem:
(defthm vl-scopestack-find-elabpath-of-vl-scopestack-fix-context-ss (equal (vl-scopestack-find-elabpath ss (vl-scopestack-fix context-ss) pkg-name) (vl-scopestack-find-elabpath ss context-ss pkg-name)))
Theorem:
(defthm vl-scopestack-find-elabpath-vl-scopestack-equiv-congruence-on-context-ss (implies (vl-scopestack-equiv context-ss context-ss-equiv) (equal (vl-scopestack-find-elabpath ss context-ss pkg-name) (vl-scopestack-find-elabpath ss context-ss-equiv pkg-name))) :rule-classes :congruence)
Theorem:
(defthm vl-scopestack-find-elabpath-of-maybe-string-fix-pkg-name (equal (vl-scopestack-find-elabpath ss context-ss (maybe-string-fix pkg-name)) (vl-scopestack-find-elabpath ss context-ss pkg-name)))
Theorem:
(defthm vl-scopestack-find-elabpath-maybe-string-equiv-congruence-on-pkg-name (implies (maybe-string-equiv pkg-name pkg-name-equiv) (equal (vl-scopestack-find-elabpath ss context-ss pkg-name) (vl-scopestack-find-elabpath ss context-ss pkg-name-equiv))) :rule-classes :congruence)