		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstmt-initialize-locals

Signature
(svstmt-initialize-locals locals) → scope
Arguments: locals — Guard (svarlist-p locals).
Returns: scope — Type (svex-alist-p scope).

Definitions and Theorems

Function: svstmt-initialize-locals

(defun svstmt-initialize-locals (locals)
  (declare (xargs :guard (svarlist-p locals)))
  (let ((__function__ 'svstmt-initialize-locals))
    (declare (ignorable __function__))
    (if (atom locals)
        nil
      (svex-fastacons (car locals)
                      (svex-x)
                      (svstmt-initialize-locals (cdr locals))))))

Theorem: svex-alist-p-of-svstmt-initialize-locals

(defthm svex-alist-p-of-svstmt-initialize-locals
  (b* ((scope (svstmt-initialize-locals locals)))
    (svex-alist-p scope))
  :rule-classes :rewrite)

Theorem: svex-lookup-in-svstmt-initialize-locals

(defthm svex-lookup-in-svstmt-initialize-locals
  (b* ((?scope (svstmt-initialize-locals locals)))
    (iff (svex-lookup x scope)
         (member (svar-fix x)
                 (svarlist-fix locals)))))

Theorem: svex-alist-vars-of-initialize-locals

(defthm svex-alist-vars-of-initialize-locals
  (b* ((?scope (svstmt-initialize-locals locals)))
    (equal (svex-alist-vars scope) nil)))

Theorem: svstmt-initialize-locals-of-svarlist-fix-locals

(defthm svstmt-initialize-locals-of-svarlist-fix-locals
  (equal (svstmt-initialize-locals (svarlist-fix locals))
         (svstmt-initialize-locals locals)))

Theorem: svstmt-initialize-locals-svarlist-equiv-congruence-on-locals

(defthm svstmt-initialize-locals-svarlist-equiv-congruence-on-locals
  (implies (svarlist-equiv locals locals-equiv)
           (equal (svstmt-initialize-locals locals)
                  (svstmt-initialize-locals locals-equiv)))
  :rule-classes :congruence)