		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhbit-eval

Signature
(lhbit-eval x env) → *
Arguments: x — Guard (lhbit-p x).; env — Guard (svex-env-p env).

Definitions and Theorems

Function: lhbit-eval

(defun lhbit-eval (x env)
  (declare (xargs :guard (and (lhbit-p x) (svex-env-p env))))
  (let ((__function__ 'lhbit-eval))
    (declare (ignorable __function__))
    (lhbit-case
         x
         :z (4vec-1z)
         :var (4vec-bit-index x.idx (svex-env-lookup x.name env)))))

Theorem: lhbit-eval-of-lhbit-fix-x

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

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

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

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

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

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

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