		Search-engine friendly clone of the ACL2 documentation.

Svex-env

Svex-env-fastlookup

Fast lookup in a fast svex-env.

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

Definitions and Theorems

Function: svex-env-fastlookup

(defun svex-env-fastlookup (var env)
  (declare (xargs :guard (and (svar-p var) (svex-env-p env))))
  (let ((__function__ 'svex-env-fastlookup))
    (declare (ignorable __function__))
    (mbe :logic (svex-env-lookup var env)
         :exec
         (let ((look (hons-get var env)))
           (if look (cdr look) (4vec-x))))))