(vl-lucid-genvar-scope name loc) → ss
Function:
(defun vl-lucid-genvar-scope (name loc) (declare (xargs :guard (and (stringp name) (vl-location-p loc)))) (let ((__function__ 'vl-lucid-genvar-scope)) (declare (ignorable __function__)) (b* ((genvar (make-vl-genvar :name name :loc loc)) (blob (make-vl-genblob :genvars (list genvar) :scopetype :vl-genarray :id (cat "<generate-array-" name ">")))) blob)))
Theorem:
(defthm vl-scope-p-of-vl-lucid-genvar-scope (b* ((ss (vl-lucid-genvar-scope name loc))) (vl-scope-p ss)) :rule-classes :rewrite)
Theorem:
(defthm vl-lucid-genvar-scope-of-str-fix-name (equal (vl-lucid-genvar-scope (str-fix name) loc) (vl-lucid-genvar-scope name loc)))
Theorem:
(defthm vl-lucid-genvar-scope-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-lucid-genvar-scope name loc) (vl-lucid-genvar-scope name-equiv loc))) :rule-classes :congruence)
Theorem:
(defthm vl-lucid-genvar-scope-of-vl-location-fix-loc (equal (vl-lucid-genvar-scope name (vl-location-fix loc)) (vl-lucid-genvar-scope name loc)))
Theorem:
(defthm vl-lucid-genvar-scope-vl-location-equiv-congruence-on-loc (implies (vl-location-equiv loc loc-equiv) (equal (vl-lucid-genvar-scope name loc) (vl-lucid-genvar-scope name loc-equiv))) :rule-classes :congruence)