Main loop to check each index/dimension pair.
(vl-follow-hidexpr-dimscheck-aux name indices dims &key strictp) → err
Function:
(defun vl-follow-hidexpr-dimscheck-aux-fn (name indices dims strictp) (declare (xargs :guard (and (stringp name) (vl-exprlist-p indices) (vl-dimensionlist-p dims) (booleanp strictp)))) (declare (xargs :guard (same-lengthp indices dims))) (let ((__function__ 'vl-follow-hidexpr-dimscheck-aux)) (declare (ignorable __function__)) (if (atom indices) nil (or (vl-follow-hidexpr-dimcheck name (car indices) (car dims) :strictp strictp) (vl-follow-hidexpr-dimscheck-aux name (cdr indices) (cdr dims) :strictp strictp)))))
Theorem:
(defthm return-type-of-vl-follow-hidexpr-dimscheck-aux (b* ((err (vl-follow-hidexpr-dimscheck-aux-fn name indices dims strictp))) (iff (vl-msg-p err) err)) :rule-classes :rewrite)
Theorem:
(defthm vl-follow-hidexpr-dimscheck-aux-fn-of-str-fix-name (equal (vl-follow-hidexpr-dimscheck-aux-fn (str-fix name) indices dims strictp) (vl-follow-hidexpr-dimscheck-aux-fn name indices dims strictp)))
Theorem:
(defthm vl-follow-hidexpr-dimscheck-aux-fn-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-follow-hidexpr-dimscheck-aux-fn name indices dims strictp) (vl-follow-hidexpr-dimscheck-aux-fn name-equiv indices dims strictp))) :rule-classes :congruence)
Theorem:
(defthm vl-follow-hidexpr-dimscheck-aux-fn-of-vl-exprlist-fix-indices (equal (vl-follow-hidexpr-dimscheck-aux-fn name (vl-exprlist-fix indices) dims strictp) (vl-follow-hidexpr-dimscheck-aux-fn name indices dims strictp)))
Theorem:
(defthm vl-follow-hidexpr-dimscheck-aux-fn-vl-exprlist-equiv-congruence-on-indices (implies (vl-exprlist-equiv indices indices-equiv) (equal (vl-follow-hidexpr-dimscheck-aux-fn name indices dims strictp) (vl-follow-hidexpr-dimscheck-aux-fn name indices-equiv dims strictp))) :rule-classes :congruence)
Theorem:
(defthm vl-follow-hidexpr-dimscheck-aux-fn-of-vl-dimensionlist-fix-dims (equal (vl-follow-hidexpr-dimscheck-aux-fn name indices (vl-dimensionlist-fix dims) strictp) (vl-follow-hidexpr-dimscheck-aux-fn name indices dims strictp)))
Theorem:
(defthm vl-follow-hidexpr-dimscheck-aux-fn-vl-dimensionlist-equiv-congruence-on-dims (implies (vl-dimensionlist-equiv dims dims-equiv) (equal (vl-follow-hidexpr-dimscheck-aux-fn name indices dims strictp) (vl-follow-hidexpr-dimscheck-aux-fn name indices dims-equiv strictp))) :rule-classes :congruence)
Theorem:
(defthm vl-follow-hidexpr-dimscheck-aux-fn-of-bool-fix-strictp (equal (vl-follow-hidexpr-dimscheck-aux-fn name indices dims (acl2::bool-fix strictp)) (vl-follow-hidexpr-dimscheck-aux-fn name indices dims strictp)))
Theorem:
(defthm vl-follow-hidexpr-dimscheck-aux-fn-iff-congruence-on-strictp (implies (iff strictp strictp-equiv) (equal (vl-follow-hidexpr-dimscheck-aux-fn name indices dims strictp) (vl-follow-hidexpr-dimscheck-aux-fn name indices dims strictp-equiv))) :rule-classes :congruence)