		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstack-lookup

Signature
(svstack-lookup k stack) → value?
Arguments: k — Guard (svar-p k).; stack — Guard (svstack-p stack).
Returns: value? — Type (iff (svex-p value?) value?).

Definitions and Theorems

Function: svstack-lookup

(defun svstack-lookup (k stack)
  (declare (xargs :guard (and (svar-p k) (svstack-p stack))))
  (let ((__function__ 'svstack-lookup))
    (declare (ignorable __function__))
    (if (atom stack)
        nil
      (or (svex-fastlookup k (car stack))
          (svstack-lookup k (cdr stack))))))

Theorem: return-type-of-svstack-lookup

(defthm return-type-of-svstack-lookup
  (b* ((value? (svstack-lookup k stack)))
    (iff (svex-p value?) value?))
  :rule-classes :rewrite)

Theorem: svstack-lookup-in-terms-of-svex-alist

(defthm svstack-lookup-in-terms-of-svex-alist
  (b* ((?value? (svstack-lookup k stack)))
    (equal value?
           (svex-lookup k (svstack-to-svex-alist stack)))))

Theorem: svstack-lookup-of-svar-fix-k

(defthm svstack-lookup-of-svar-fix-k
  (equal (svstack-lookup (svar-fix k) stack)
         (svstack-lookup k stack)))

Theorem: svstack-lookup-svar-equiv-congruence-on-k

(defthm svstack-lookup-svar-equiv-congruence-on-k
  (implies (svar-equiv k k-equiv)
           (equal (svstack-lookup k stack)
                  (svstack-lookup k-equiv stack)))
  :rule-classes :congruence)

Theorem: svstack-lookup-of-svstack-fix-stack

(defthm svstack-lookup-of-svstack-fix-stack
  (equal (svstack-lookup k (svstack-fix stack))
         (svstack-lookup k stack)))

Theorem: svstack-lookup-svstack-equiv-congruence-on-stack

(defthm svstack-lookup-svstack-equiv-congruence-on-stack
  (implies (svstack-equiv stack stack-equiv)
           (equal (svstack-lookup k stack)
                  (svstack-lookup k stack-equiv)))
  :rule-classes :congruence)