		Search-engine friendly clone of the ACL2 documentation.

Lhrange

Lhrange-eval

Signature
(lhrange-eval x env) → val
Arguments: x — Guard (lhrange-p x).; env — Guard (svex-env-p env).
Returns: val — Type (4vec-p val).

Definitions and Theorems

Function: lhrange-eval

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

Theorem: 4vec-p-of-lhrange-eval

(defthm 4vec-p-of-lhrange-eval
  (b* ((val (lhrange-eval x env)))
    (4vec-p val))
  :rule-classes :rewrite)

Theorem: lhrange-eval-of-lhrange-fix-x

(defthm lhrange-eval-of-lhrange-fix-x
  (equal (lhrange-eval (lhrange-fix x) env)
         (lhrange-eval x env)))

Theorem: lhrange-eval-lhrange-equiv-congruence-on-x

(defthm lhrange-eval-lhrange-equiv-congruence-on-x
  (implies (lhrange-equiv x x-equiv)
           (equal (lhrange-eval x env)
                  (lhrange-eval x-equiv env)))
  :rule-classes :congruence)

Theorem: lhrange-eval-of-svex-env-fix-env

(defthm lhrange-eval-of-svex-env-fix-env
  (equal (lhrange-eval x (svex-env-fix env))
         (lhrange-eval x env)))

Theorem: lhrange-eval-svex-env-equiv-congruence-on-env

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