Generate a bunch of module instances.
(vl-simple-instantiate-list x prefix arglists &key (n '0) (loc '*vl-fakeloc*)) → insts
Function:
(defun vl-simple-instantiate-list-fn (x prefix arglists n loc) (declare (xargs :guard (and (vl-module-p x) (stringp prefix) (vl-exprlistlist-p arglists) (natp n) (vl-location-p loc)))) (let ((__function__ 'vl-simple-instantiate-list)) (declare (ignorable __function__)) (if (atom arglists) nil (cons (vl-simple-instantiate x (cat prefix (natstr n)) (car arglists) :loc loc) (vl-simple-instantiate-list-fn x prefix (cdr arglists) (+ 1 (lnfix n)) loc)))))
Theorem:
(defthm vl-modinstlist-p-of-vl-simple-instantiate-list (b* ((insts (vl-simple-instantiate-list-fn x prefix arglists n loc))) (vl-modinstlist-p insts)) :rule-classes :rewrite)
Theorem:
(defthm vl-simple-instantiate-list-fn-of-vl-module-fix-x (equal (vl-simple-instantiate-list-fn (vl-module-fix x) prefix arglists n loc) (vl-simple-instantiate-list-fn x prefix arglists n loc)))
Theorem:
(defthm vl-simple-instantiate-list-fn-vl-module-equiv-congruence-on-x (implies (vl-module-equiv x x-equiv) (equal (vl-simple-instantiate-list-fn x prefix arglists n loc) (vl-simple-instantiate-list-fn x-equiv prefix arglists n loc))) :rule-classes :congruence)
Theorem:
(defthm vl-simple-instantiate-list-fn-of-str-fix-prefix (equal (vl-simple-instantiate-list-fn x (str-fix prefix) arglists n loc) (vl-simple-instantiate-list-fn x prefix arglists n loc)))
Theorem:
(defthm vl-simple-instantiate-list-fn-streqv-congruence-on-prefix (implies (streqv prefix prefix-equiv) (equal (vl-simple-instantiate-list-fn x prefix arglists n loc) (vl-simple-instantiate-list-fn x prefix-equiv arglists n loc))) :rule-classes :congruence)
Theorem:
(defthm vl-simple-instantiate-list-fn-of-vl-exprlistlist-fix-arglists (equal (vl-simple-instantiate-list-fn x prefix (vl-exprlistlist-fix arglists) n loc) (vl-simple-instantiate-list-fn x prefix arglists n loc)))
Theorem:
(defthm vl-simple-instantiate-list-fn-vl-exprlistlist-equiv-congruence-on-arglists (implies (vl-exprlistlist-equiv arglists arglists-equiv) (equal (vl-simple-instantiate-list-fn x prefix arglists n loc) (vl-simple-instantiate-list-fn x prefix arglists-equiv n loc))) :rule-classes :congruence)
Theorem:
(defthm vl-simple-instantiate-list-fn-of-nfix-n (equal (vl-simple-instantiate-list-fn x prefix arglists (nfix n) loc) (vl-simple-instantiate-list-fn x prefix arglists n loc)))
Theorem:
(defthm vl-simple-instantiate-list-fn-nat-equiv-congruence-on-n (implies (acl2::nat-equiv n n-equiv) (equal (vl-simple-instantiate-list-fn x prefix arglists n loc) (vl-simple-instantiate-list-fn x prefix arglists n-equiv loc))) :rule-classes :congruence)
Theorem:
(defthm vl-simple-instantiate-list-fn-of-vl-location-fix-loc (equal (vl-simple-instantiate-list-fn x prefix arglists n (vl-location-fix loc)) (vl-simple-instantiate-list-fn x prefix arglists n loc)))
Theorem:
(defthm vl-simple-instantiate-list-fn-vl-location-equiv-congruence-on-loc (implies (vl-location-equiv loc loc-equiv) (equal (vl-simple-instantiate-list-fn x prefix arglists n loc) (vl-simple-instantiate-list-fn x prefix arglists n loc-equiv))) :rule-classes :congruence)