		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)