		Search-engine friendly clone of the ACL2 documentation.

Lhatom

Lhatom->svex

Signature
(lhatom->svex x) → xx
Arguments: x — Guard (lhatom-p x).
Returns: xx — Type (svex-p xx).

Definitions and Theorems

Function: lhatom->svex

(defun lhatom->svex (x)
  (declare (xargs :guard (lhatom-p x)))
  (let ((__function__ 'lhatom->svex))
    (declare (ignorable __function__))
    (lhatom-case x
                 :z (svex-quote (4vec-z))
                 :var (svex-rsh x.rsh (svex-var x.name)))))

Theorem: svex-p-of-lhatom->svex

(defthm svex-p-of-lhatom->svex
  (b* ((xx (lhatom->svex x))) (svex-p xx))
  :rule-classes :rewrite)

Theorem: lhatom->svex-of-lhatom-fix-x

(defthm lhatom->svex-of-lhatom-fix-x
  (equal (lhatom->svex (lhatom-fix x))
         (lhatom->svex x)))

Theorem: lhatom->svex-lhatom-equiv-congruence-on-x

(defthm lhatom->svex-lhatom-equiv-congruence-on-x
  (implies (lhatom-equiv x x-equiv)
           (equal (lhatom->svex x)
                  (lhatom->svex x-equiv)))
  :rule-classes :congruence)

Theorem: lhatom->svex-correct

(defthm lhatom->svex-correct
  (equal (svex-eval (lhatom->svex x) env)
         (lhatom-eval x env)))