		Search-engine friendly clone of the ACL2 documentation.

Following-hids

Vl-genarrayblocklist-find-block

Find the block from a generate array corresponding to some index.

Signature
(vl-genarrayblocklist-find-block idx x) → blk
Arguments: idx — Guard (integerp idx).; x — Guard (vl-genarrayblocklist-p x).
Returns: blk — Type (iff (vl-genarrayblock-p blk) blk).

Definitions and Theorems

Function: vl-genarrayblocklist-find-block

(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: return-type-of-vl-genarrayblocklist-find-block

(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: vl-genarrayblocklist-find-block-of-ifix-idx

(defthm vl-genarrayblocklist-find-block-of-ifix-idx
  (equal (vl-genarrayblocklist-find-block (ifix idx)
                                          x)
         (vl-genarrayblocklist-find-block idx x)))

Theorem: vl-genarrayblocklist-find-block-int-equiv-congruence-on-idx

(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: vl-genarrayblocklist-find-block-of-vl-genarrayblocklist-fix-x

(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: vl-genarrayblocklist-find-block-vl-genarrayblocklist-equiv-congruence-on-x

(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)