Find the block from a generate array corresponding to some index.
(vl-genarrayblocklist-find-block idx x) → blk
Function:
(defun vl-genarrayblocklist-find-block (idx x) (declare (xargs :guard (and (integerp idx) (vl-genarrayblocklist-p x)))) (let ((__function__ 'vl-genarrayblocklist-find-block)) (declare (ignorable __function__)) (cond ((atom x) nil) ((eql (vl-genarrayblock->index (car x)) (lifix idx)) (vl-genarrayblock-fix (car x))) (t (vl-genarrayblocklist-find-block idx (cdr x))))))
Theorem:
(defthm return-type-of-vl-genarrayblocklist-find-block (b* ((blk (vl-genarrayblocklist-find-block idx x))) (iff (vl-genarrayblock-p blk) blk)) :rule-classes :rewrite)
Theorem:
(defthm vl-genarrayblocklist-find-block-of-ifix-idx (equal (vl-genarrayblocklist-find-block (ifix idx) x) (vl-genarrayblocklist-find-block idx x)))
Theorem:
(defthm vl-genarrayblocklist-find-block-int-equiv-congruence-on-idx (implies (acl2::int-equiv idx idx-equiv) (equal (vl-genarrayblocklist-find-block idx x) (vl-genarrayblocklist-find-block idx-equiv x))) :rule-classes :congruence)
Theorem:
(defthm vl-genarrayblocklist-find-block-of-vl-genarrayblocklist-fix-x (equal (vl-genarrayblocklist-find-block idx (vl-genarrayblocklist-fix x)) (vl-genarrayblocklist-find-block idx x)))
Theorem:
(defthm vl-genarrayblocklist-find-block-vl-genarrayblocklist-equiv-congruence-on-x (implies (vl-genarrayblocklist-equiv x x-equiv) (equal (vl-genarrayblocklist-find-block idx x) (vl-genarrayblocklist-find-block idx x-equiv))) :rule-classes :congruence)