		Search-engine friendly clone of the ACL2 documentation.

Hid-tools

Vl-seltrace->indices

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

Definitions and Theorems

Function: vl-seltrace->indices

(defun vl-seltrace->indices (x)
  (declare (xargs :guard (vl-seltrace-p x)))
  (let ((__function__ 'vl-seltrace->indices))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (b* (((vl-selstep x1) (car x)))
        (vl-select-case
             x1.select
             :field (vl-seltrace->indices (cdr x))
             :index (cons x1.select.val
                          (vl-seltrace->indices (cdr x))))))))

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

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

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

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

Theorem: vl-seltrace-indices-of-append

(defthm vl-seltrace-indices-of-append
  (equal (vl-seltrace->indices (append x y))
         (append (vl-seltrace->indices x)
                 (vl-seltrace->indices y))))

Theorem: vl-seltrace-indices-of-rev

(defthm vl-seltrace-indices-of-rev
  (equal (vl-seltrace->indices (rev x))
         (rev (vl-seltrace->indices x))))

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

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

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

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