		Search-engine friendly clone of the ACL2 documentation.

Svex-alist

Svex-fastlookup

Fast lookup in an svex-alist.

Signature
(svex-fastlookup var a) → *
Arguments: var — Guard (svar-p var).; a — Guard (svex-alist-p a).

Definitions and Theorems

Function: svex-fastlookup$inline

(defun svex-fastlookup$inline (var a)
  (declare (xargs :guard (and (svar-p var) (svex-alist-p a))))
  (let ((__function__ 'svex-fastlookup))
    (declare (ignorable __function__))
    (mbe :logic (svex-lookup var a)
         :exec (cdr (hons-get var a)))))

Theorem: svex-fastlookup$inline-of-svar-fix-var

(defthm svex-fastlookup$inline-of-svar-fix-var
  (equal (svex-fastlookup$inline (svar-fix var)
                                 a)
         (svex-fastlookup$inline var a)))

Theorem: svex-fastlookup$inline-svar-equiv-congruence-on-var

(defthm svex-fastlookup$inline-svar-equiv-congruence-on-var
  (implies (svar-equiv var var-equiv)
           (equal (svex-fastlookup$inline var a)
                  (svex-fastlookup$inline var-equiv a)))
  :rule-classes :congruence)

Theorem: svex-fastlookup$inline-of-svex-alist-fix-a

(defthm svex-fastlookup$inline-of-svex-alist-fix-a
  (equal (svex-fastlookup$inline var (svex-alist-fix a))
         (svex-fastlookup$inline var a)))

Theorem: svex-fastlookup$inline-svex-alist-equiv-congruence-on-a

(defthm svex-fastlookup$inline-svex-alist-equiv-congruence-on-a
  (implies (svex-alist-equiv a a-equiv)
           (equal (svex-fastlookup$inline var a)
                  (svex-fastlookup$inline var a-equiv)))
  :rule-classes :congruence)