		Search-engine friendly clone of the ACL2 documentation.

Svex-alist

Svex-lookup

Slow lookup in an svex-alist.

Signature
(svex-lookup var a) → value?
Arguments: var — Guard (svar-p var).; a — Guard (svex-alist-p a).
Returns: value? — Type (iff (svex-p value?) value?).

Definitions and Theorems

Function: svex-lookup

(defun svex-lookup (var a)
  (declare (xargs :guard (and (svar-p var) (svex-alist-p a))))
  (let ((__function__ 'svex-lookup))
    (declare (ignorable __function__))
    (mbe :logic (cdr (hons-assoc-equal (svar-fix var)
                                       (svex-alist-fix a)))
         :exec (cdr (assoc-equal var a)))))

Theorem: return-type-of-svex-lookup

(defthm return-type-of-svex-lookup
  (b* ((value? (svex-lookup var a)))
    (iff (svex-p value?) value?))
  :rule-classes :rewrite)

Theorem: svex-lookup-of-svar-fix-var

(defthm svex-lookup-of-svar-fix-var
  (equal (svex-lookup (svar-fix var) a)
         (svex-lookup var a)))

Theorem: svex-lookup-svar-equiv-congruence-on-var

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

Theorem: svex-lookup-of-svex-alist-fix-a

(defthm svex-lookup-of-svex-alist-fix-a
  (equal (svex-lookup var (svex-alist-fix a))
         (svex-lookup var a)))

Theorem: svex-lookup-svex-alist-equiv-congruence-on-a

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

Theorem: svex-lookup-of-nil

(defthm svex-lookup-of-nil
  (equal (svex-lookup v nil) nil))

Theorem: svex-lookup-of-svex-acons

(defthm svex-lookup-of-svex-acons
  (equal (svex-lookup var1 (svex-acons var2 x a))
         (if (equal (svar-fix var1) (svar-fix var2))
             (svex-fix x)
           (svex-lookup var1 a))))