		Search-engine friendly clone of the ACL2 documentation.

Svex-select

Svex-select-inner-width

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

Definitions and Theorems

Function: svex-select-inner-width

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

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

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

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

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

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

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