		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhatom-eval-zero

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

Definitions and Theorems

Function: lhatom-eval-zero

(defun lhatom-eval-zero (x env)
  (declare (xargs :guard (and (lhatom-p x) (svex-env-p env))))
  (let ((__function__ 'lhatom-eval-zero))
    (declare (ignorable __function__))
    (lhatom-case x
                 :z 0
                 :var (4vec-rsh (2vec x.rsh)
                                (svex-env-fastlookup x.name env)))))

Theorem: 4vec-p-of-lhatom-eval-zero

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

Theorem: lhatom-eval-zero-of-lhatom-fix-x

(defthm lhatom-eval-zero-of-lhatom-fix-x
  (equal (lhatom-eval-zero (lhatom-fix x) env)
         (lhatom-eval-zero x env)))

Theorem: lhatom-eval-zero-lhatom-equiv-congruence-on-x

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

Theorem: lhatom-eval-zero-of-svex-env-fix-env

(defthm lhatom-eval-zero-of-svex-env-fix-env
  (equal (lhatom-eval-zero x (svex-env-fix env))
         (lhatom-eval-zero x env)))

Theorem: lhatom-eval-zero-svex-env-equiv-congruence-on-env

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