		Search-engine friendly clone of the ACL2 documentation.

Elaborate

Sv::svex-constval

Signature
(sv::svex-constval acl2::x) → sv::val
Arguments: acl2::x — Guard (sv::svex-p acl2::x).
Returns: sv::val — Type (sv::maybe-4vec-p sv::val).

Definitions and Theorems

Function: svex-constval

(defun sv::svex-constval (acl2::x)
  (declare (xargs :guard (sv::svex-p acl2::x)))
  (let ((__function__ 'sv::svex-constval))
    (declare (ignorable __function__))
    (sv::svex-case acl2::x
                   :quote sv::x.val
                   :otherwise nil)))

Theorem: maybe-4vec-p-of-svex-constval

(defthm sv::maybe-4vec-p-of-svex-constval
  (b* ((sv::val (sv::svex-constval acl2::x)))
    (sv::maybe-4vec-p sv::val))
  :rule-classes :rewrite)

Theorem: svex-constval-of-svex-fix-x

(defthm sv::svex-constval-of-svex-fix-x
  (equal (sv::svex-constval (sv::svex-fix acl2::x))
         (sv::svex-constval acl2::x)))

Theorem: svex-constval-svex-equiv-congruence-on-x

(defthm sv::svex-constval-svex-equiv-congruence-on-x
  (implies (sv::svex-equiv acl2::x sv::x-equiv)
           (equal (sv::svex-constval acl2::x)
                  (sv::svex-constval sv::x-equiv)))
  :rule-classes :congruence)