(vl-scopeitem->loc x) → loc
Function:
(defun vl-scopeitem->loc (x) (declare (xargs :guard (vl-scopeitem-p x))) (let ((__function__ 'vl-scopeitem->loc)) (declare (ignorable __function__)) (let ((x (vl-scopeitem-fix x))) (case (tag x) ((:vl-genloop :vl-genif :vl-gencase :vl-genbegin :vl-genarray :vl-genbase) (vl-genelement->loc x)) ((:vl-interfaceport) (vl-interfaceport->loc x)) (t (vl-modelement->loc x))))))
Theorem:
(defthm vl-location-p-of-vl-scopeitem->loc (b* ((loc (vl-scopeitem->loc x))) (vl-location-p loc)) :rule-classes :rewrite)
Theorem:
(defthm vl-scopeitem->loc-of-vl-scopeitem-fix-x (equal (vl-scopeitem->loc (vl-scopeitem-fix x)) (vl-scopeitem->loc x)))
Theorem:
(defthm vl-scopeitem->loc-vl-scopeitem-equiv-congruence-on-x (implies (vl-scopeitem-equiv x x-equiv) (equal (vl-scopeitem->loc x) (vl-scopeitem->loc x-equiv))) :rule-classes :congruence)