		Search-engine friendly clone of the ACL2 documentation.

Lhrange

Lhrange->svex

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

Definitions and Theorems

Function: lhrange->svex

(defun lhrange->svex (x)
  (declare (xargs :guard (lhrange-p x)))
  (let ((__function__ 'lhrange->svex))
    (declare (ignorable __function__))
    (b* (((lhrange x) x))
      (svcall* concat (svex-quote (2vec x.w))
               (lhatom->svex x.atom)
               (svex-quote (4vec-z))))))

Theorem: svex-p-of-lhrange->svex

(defthm svex-p-of-lhrange->svex
  (b* ((s (lhrange->svex x))) (svex-p s))
  :rule-classes :rewrite)

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

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

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

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

Theorem: lhrange->svex-correct

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