		Search-engine friendly clone of the ACL2 documentation.

Bfr-lookup

Look up a BFR variable in an appropriate BDD/AIG environment.

Signature
(bfr-lookup n env) → *
Arguments: n — Guard (bfr-varname-p n).

Definitions and Theorems

Function: bfr-lookup

(defun bfr-lookup (n env)
  (declare (xargs :guard (bfr-varname-p n)))
  (let ((__function__ 'bfr-lookup))
    (declare (ignorable __function__))
    (let ((n (bfr-varname-fix n)))
      (bfr-case
           :bdd (and (with-guard-checking nil (ec-call (nth n env)))
                     t)
           :aig (acl2::aig-env-lookup n env)))))

Theorem: bfr-varname-equiv-implies-equal-bfr-lookup-1

(defthm bfr-varname-equiv-implies-equal-bfr-lookup-1
  (implies (bfr-varname-equiv n n-equiv)
           (equal (bfr-lookup n env)
                  (bfr-lookup n-equiv env)))
  :rule-classes (:congruence))