		Search-engine friendly clone of the ACL2 documentation.

Svex-select

Svex-select->width

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

Definitions and Theorems

Function: svex-select->width

(defun svex-select->width (x)
  (declare (xargs :guard (svex-select-p x)))
  (let ((__function__ 'svex-select->width))
    (declare (ignorable __function__))
    (svex-select-case x
                      :var x.width
                      :part x.width)))

Theorem: natp-of-svex-select->width

(defthm natp-of-svex-select->width
  (b* ((width (svex-select->width x)))
    (natp width))
  :rule-classes :type-prescription)

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

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

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

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