		Search-engine friendly clone of the ACL2 documentation.

Compile.lisp

Delay-svarlist->delays

Signature
(delay-svarlist->delays x) → delays
Arguments: x — Guard (svarlist-p x).
Returns: delays — Type (svar-map-p delays).

Definitions and Theorems

Function: delay-svarlist->delays

(defun delay-svarlist->delays (x)
       (declare (xargs :guard (svarlist-p x)))
       (let ((__function__ 'delay-svarlist->delays))
            (declare (ignorable __function__))
            (b* (((when (atom x)) nil)
                 (rest (delay-svarlist->delays (cdr x)))
                 (delays1 (delay-svar->delays (car x))))
                (append-without-guard delays1 rest))))

Theorem: svar-map-p-of-delay-svarlist->delays

(defthm svar-map-p-of-delay-svarlist->delays
        (b* ((delays (delay-svarlist->delays x)))
            (svar-map-p delays))
        :rule-classes :rewrite)

Theorem: vars-of-delay-svarlist->delays

(defthm vars-of-delay-svarlist->delays
        (b* ((?delays (delay-svarlist->delays x)))
            (implies (svarlist-addr-p x)
                     (svarlist-addr-p (svar-map-vars delays)))))

Theorem: vars-of-delay-svarlist->delays-alist-vals

(defthm vars-of-delay-svarlist->delays-alist-vals
        (b* ((?delays (delay-svarlist->delays x)))
            (implies (svarlist-addr-p x)
                     (svarlist-addr-p (alist-vals delays)))))

Theorem: vars-of-delay-svarlist->delays-alist-keys

(defthm vars-of-delay-svarlist->delays-alist-keys
        (b* ((?delays (delay-svarlist->delays x)))
            (implies (svarlist-addr-p x)
                     (svarlist-addr-p (alist-keys delays)))))

Theorem: delay-svarlist->delays-of-svarlist-fix-x

(defthm delay-svarlist->delays-of-svarlist-fix-x
        (equal (delay-svarlist->delays (svarlist-fix x))
               (delay-svarlist->delays x)))

Theorem: delay-svarlist->delays-svarlist-equiv-congruence-on-x

(defthm delay-svarlist->delays-svarlist-equiv-congruence-on-x
        (implies (svarlist-equiv x x-equiv)
                 (equal (delay-svarlist->delays x)
                        (delay-svarlist->delays x-equiv)))
        :rule-classes :congruence)