		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-value-to-svex

Signature
(vl-value-to-svex x) → (mv err svex)
Arguments: x — Guard (vl-value-p x).
Returns: err — Type (iff (vl-msg-p err) err).; svex — Type (sv::svex-p svex).

Definitions and Theorems

Function: vl-value-to-svex

(defun vl-value-to-svex (x)
  (declare (xargs :guard (vl-value-p x)))
  (let ((__function__ 'vl-value-to-svex))
    (declare (ignorable __function__))
    (b* (((mv err 4vec) (vl-value-to-4vec x)))
      (mv err (sv::svex-quote 4vec)))))

Theorem: return-type-of-vl-value-to-svex.err

(defthm return-type-of-vl-value-to-svex.err
  (b* (((mv ?err ?svex) (vl-value-to-svex x)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: svex-p-of-vl-value-to-svex.svex

(defthm svex-p-of-vl-value-to-svex.svex
  (b* (((mv ?err ?svex) (vl-value-to-svex x)))
    (sv::svex-p svex))
  :rule-classes :rewrite)

Theorem: vars-of-vl-value-to-svex

(defthm vars-of-vl-value-to-svex
  (b* (((mv ?err ?svex) (vl-value-to-svex x)))
    (equal (sv::svex-vars svex) nil)))

Theorem: vl-value-to-svex-of-vl-value-fix-x

(defthm vl-value-to-svex-of-vl-value-fix-x
  (equal (vl-value-to-svex (vl-value-fix x))
         (vl-value-to-svex x)))

Theorem: vl-value-to-svex-vl-value-equiv-congruence-on-x

(defthm vl-value-to-svex-vl-value-equiv-congruence-on-x
  (implies (vl-value-equiv x x-equiv)
           (equal (vl-value-to-svex x)
                  (vl-value-to-svex x-equiv)))
  :rule-classes :congruence)