		Search-engine friendly clone of the ACL2 documentation.

Hid-tools

Vl-operandinfo->indices

Signature
(vl-operandinfo->indices x) → indices
Arguments: x — Guard (vl-operandinfo-p x).
Returns: indices — Type (vl-exprlist-p indices).

Definitions and Theorems

Function: vl-operandinfo->indices

(defun vl-operandinfo->indices (x)
 (declare (xargs :guard (vl-operandinfo-p x)))
 (let ((__function__ 'vl-operandinfo->indices))
  (declare (ignorable __function__))
  (b* (((vl-operandinfo x)))
   (append
     (vl-partselect-case x.part
                         :none nil
                         :range (list x.part.msb x.part.lsb)
                         :plusminus (list x.part.base x.part.width))
     (vl-seltrace->indices x.seltrace)))))

Theorem: vl-exprlist-p-of-vl-operandinfo->indices

(defthm vl-exprlist-p-of-vl-operandinfo->indices
  (b* ((indices (vl-operandinfo->indices x)))
    (vl-exprlist-p indices))
  :rule-classes :rewrite)

Theorem: len-of-vl-operandinfo->indices

(defthm len-of-vl-operandinfo->indices
  (b* ((?indices (vl-operandinfo->indices x)))
    (equal (len indices)
           (vl-operandinfo-index-count x))))

Theorem: vl-operandinfo->indices-of-vl-operandinfo-fix-x

(defthm vl-operandinfo->indices-of-vl-operandinfo-fix-x
  (equal (vl-operandinfo->indices (vl-operandinfo-fix x))
         (vl-operandinfo->indices x)))

Theorem: vl-operandinfo->indices-vl-operandinfo-equiv-congruence-on-x

(defthm vl-operandinfo->indices-vl-operandinfo-equiv-congruence-on-x
  (implies (vl-operandinfo-equiv x x-equiv)
           (equal (vl-operandinfo->indices x)
                  (vl-operandinfo->indices x-equiv)))
  :rule-classes :congruence)