		Search-engine friendly clone of the ACL2 documentation.

Truth

Env-lookup

Signature
(env-lookup var env) → *
Arguments: var — Guard (natp var).; env — Guard (natp env).

Definitions and Theorems

Function: env-lookup

(defun env-lookup (var env)
       (declare (xargs :guard (and (natp var) (natp env))))
       (let ((__function__ 'env-lookup))
            (declare (ignorable __function__))
            (logbitp (lnfix var) (lnfix env))))

Theorem: env-lookup-of-nfix-var

(defthm env-lookup-of-nfix-var
        (equal (env-lookup (nfix var) env)
               (env-lookup var env)))

Theorem: env-lookup-nat-equiv-congruence-on-var

(defthm env-lookup-nat-equiv-congruence-on-var
        (implies (nat-equiv var var-equiv)
                 (equal (env-lookup var env)
                        (env-lookup var-equiv env)))
        :rule-classes :congruence)

Theorem: env-lookup-of-nfix-env

(defthm env-lookup-of-nfix-env
        (equal (env-lookup var (nfix env))
               (env-lookup var env)))

Theorem: env-lookup-nat-equiv-congruence-on-env

(defthm env-lookup-nat-equiv-congruence-on-env
        (implies (nat-equiv env env-equiv)
                 (equal (env-lookup var env)
                        (env-lookup var env-equiv)))
        :rule-classes :congruence)