		Search-engine friendly clone of the ACL2 documentation.

Svex-select

Svex-select-inner-var

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

Definitions and Theorems

Function: svex-select-inner-var

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

Theorem: svar-p-of-svex-select-inner-var

(defthm svar-p-of-svex-select-inner-var
  (b* ((var (svex-select-inner-var x)))
    (svar-p var))
  :rule-classes :rewrite)

Theorem: svex-select-inner-var-of-replace-indices

(defthm svex-select-inner-var-of-replace-indices
 (equal
     (svex-select-inner-var (svex-select-replace-indices x indices))
     (svex-select-inner-var x)))

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

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

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

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