		Search-engine friendly clone of the ACL2 documentation.

Svex-select

Svex-select-staticp

Signature
(svex-select-staticp x) → *
Arguments: x — Guard (svex-select-p x).

Definitions and Theorems

Function: svex-select-staticp

(defun svex-select-staticp (x)
  (declare (xargs :guard (svex-select-p x)))
  (let ((__function__ 'svex-select-staticp))
    (declare (ignorable __function__))
    (svex-select-case
         x
         :var t
         :part (and (svex-case x.lsb
                               :quote (4vec-index-p x.lsb.val)
                               :otherwise nil)
                    (svex-select-staticp x.subexp)))))

Theorem: svex-select-staticp-when-var

(defthm svex-select-staticp-when-var
  (implies (svex-select-case x :var)
           (svex-select-staticp x)))

Theorem: svex-select-vars-when-staticp

(defthm svex-select-vars-when-staticp
  (implies (svex-select-staticp x)
           (equal (svex-select-vars x)
                  (list (svex-select-inner-var x)))))

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

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

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

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