		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)