		Search-engine friendly clone of the ACL2 documentation.

Svex-select

Svex-select-to-svex

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

Definitions and Theorems

Function: svex-select-to-svex

(defun svex-select-to-svex (x)
  (declare (xargs :guard (svex-select-p x)))
  (let ((__function__ 'svex-select-to-svex))
    (declare (ignorable __function__))
    (svex-select-case
         x
         :var (svex-var x.name)
         :part (svcall partsel x.lsb (svex-int x.width)
                       (svex-concat (svex-select->width x.subexp)
                                    (svex-select-to-svex x.subexp)
                                    (svex-x))))))

Theorem: svex-p-of-svex-select-to-svex

(defthm svex-p-of-svex-select-to-svex
  (b* ((svex-x (svex-select-to-svex x)))
    (svex-p svex-x))
  :rule-classes :rewrite)

Theorem: svex-select-to-svex-of-svex-select-fix-x

(defthm svex-select-to-svex-of-svex-select-fix-x
  (equal (svex-select-to-svex (svex-select-fix x))
         (svex-select-to-svex x)))

Theorem: svex-select-to-svex-svex-select-equiv-congruence-on-x

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