		Search-engine friendly clone of the ACL2 documentation.

Svex-select

Svex-select->indices

Signature
(svex-select->indices x) → indices
Arguments: x — Guard (svex-select-p x).
Returns: indices — Type (svexlist-p indices).

Definitions and Theorems

Function: svex-select->indices

(defun svex-select->indices (x)
 (declare (xargs :guard (svex-select-p x)))
 (declare (xargs :guard (svex-select-p x)))
 (let ((__function__ 'svex-select->indices))
   (declare (ignorable __function__))
   (svex-select-case x
                     :var nil
                     :part (cons x.lsb
                                 (svex-select->indices x.subexp)))))

Theorem: svexlist-p-of-svex-select->indices

(defthm svexlist-p-of-svex-select->indices
  (b* ((indices (svex-select->indices x)))
    (svexlist-p indices))
  :rule-classes :rewrite)

Theorem: svex-select->indices-of-svex-select-fix-x

(defthm svex-select->indices-of-svex-select-fix-x
  (equal (svex-select->indices (svex-select-fix x))
         (svex-select->indices x)))

Theorem: svex-select->indices-svex-select-equiv-congruence-on-x

(defthm svex-select->indices-svex-select-equiv-congruence-on-x
  (implies (svex-select-equiv x x-equiv)
           (equal (svex-select->indices x)
                  (svex-select->indices x-equiv)))
  :rule-classes :congruence)