		Search-engine friendly clone of the ACL2 documentation.

4v-lookup

Alist lookup that automatically 4v-fixes its result.

BOZO this is a convenient operation for ...

Definitions and Theorems

Function: 4v-lookup

(defun 4v-lookup (k env)
  (declare (xargs :guard t))
  (mbe :logic
       (let ((look (hons-get k env)))
         (if look (4v-fix (cdr look)) (4vx)))
       :exec
       (let ((look (hons-get k env)))
         (prog2$ (and (not look) (4v-lookup-not-found k))
                 (4v-fix (cdr look))))))

Theorem: 4vp-of-4v-lookup

(defthm 4vp-of-4v-lookup
  (4vp (4v-lookup k env)))

Theorem: 4v-fix-4v-lookup

(defthm 4v-fix-4v-lookup
  (equal (4v-fix (4v-lookup k env))
         (4v-lookup k env)))