(vl-lucid-paramdecl-for-genloop name loc) → decl
Function:
(defun vl-lucid-paramdecl-for-genloop (name loc) (declare (xargs :guard (and (stringp name) (vl-location-p loc)))) (let ((__function__ 'vl-lucid-paramdecl-for-genloop)) (declare (ignorable __function__)) (make-vl-paramdecl :name name :localp t :type (make-vl-explicitvalueparam :type *vl-plain-old-integer-type*) :loc loc)))
Theorem:
(defthm vl-paramdecl-p-of-vl-lucid-paramdecl-for-genloop (b* ((decl (vl-lucid-paramdecl-for-genloop name loc))) (vl-paramdecl-p decl)) :rule-classes :rewrite)
Theorem:
(defthm vl-lucid-paramdecl-for-genloop-of-str-fix-name (equal (vl-lucid-paramdecl-for-genloop (str-fix name) loc) (vl-lucid-paramdecl-for-genloop name loc)))
Theorem:
(defthm vl-lucid-paramdecl-for-genloop-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-lucid-paramdecl-for-genloop name loc) (vl-lucid-paramdecl-for-genloop name-equiv loc))) :rule-classes :congruence)
Theorem:
(defthm vl-lucid-paramdecl-for-genloop-of-vl-location-fix-loc (equal (vl-lucid-paramdecl-for-genloop name (vl-location-fix loc)) (vl-lucid-paramdecl-for-genloop name loc)))
Theorem:
(defthm vl-lucid-paramdecl-for-genloop-vl-location-equiv-congruence-on-loc (implies (vl-location-equiv loc loc-equiv) (equal (vl-lucid-paramdecl-for-genloop name loc) (vl-lucid-paramdecl-for-genloop name loc-equiv))) :rule-classes :congruence)