		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstack-free

Signature
(svstack-free x) → *
Arguments: x — Guard (svstack-p x).

Definitions and Theorems

Function: svstack-free

(defun svstack-free (x)
  (declare (xargs :guard (svstack-p x)))
  (let ((__function__ 'svstack-free))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (prog2$ (fast-alist-free (car x))
              (svstack-free (cdr x))))))

Theorem: svstack-free-of-svstack-fix-x

(defthm svstack-free-of-svstack-fix-x
  (equal (svstack-free (svstack-fix x))
         (svstack-free x)))

Theorem: svstack-free-svstack-equiv-congruence-on-x

(defthm svstack-free-svstack-equiv-congruence-on-x
  (implies (svstack-equiv x x-equiv)
           (equal (svstack-free x)
                  (svstack-free x-equiv)))
  :rule-classes :congruence)