		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-collect-resolved-slices

Signature
(vl-lucid-collect-resolved-slices x) → resolved
Arguments: x — Guard (vl-lucidocclist-p x).
Returns: resolved — Type (and (vl-lucidocclist-p resolved) (vl-lucid-all-slices-p resolved) (vl-lucid-all-slices-resolved-p resolved)) .

Definitions and Theorems

Function: vl-lucid-collect-resolved-slices

(defun vl-lucid-collect-resolved-slices (x)
  (declare (xargs :guard (vl-lucidocclist-p x)))
  (let ((__function__ 'vl-lucid-collect-resolved-slices))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((when (and (eq (vl-lucidocc-kind (car x)) :slice)
                     (vl-lucid-resolved-slice-p (car x))))
          (cons (vl-lucidocc-fix (car x))
                (vl-lucid-collect-resolved-slices (cdr x)))))
      (vl-lucid-collect-resolved-slices (cdr x)))))

Theorem: return-type-of-vl-lucid-collect-resolved-slices

(defthm return-type-of-vl-lucid-collect-resolved-slices
  (b* ((resolved (vl-lucid-collect-resolved-slices x)))
    (and (vl-lucidocclist-p resolved)
         (vl-lucid-all-slices-p resolved)
         (vl-lucid-all-slices-resolved-p resolved)))
  :rule-classes :rewrite)

Theorem: vl-lucid-collect-resolved-slices-of-vl-lucidocclist-fix-x

(defthm vl-lucid-collect-resolved-slices-of-vl-lucidocclist-fix-x
  (equal (vl-lucid-collect-resolved-slices (vl-lucidocclist-fix x))
         (vl-lucid-collect-resolved-slices x)))

Theorem: vl-lucid-collect-resolved-slices-vl-lucidocclist-equiv-congruence-on-x

(defthm
 vl-lucid-collect-resolved-slices-vl-lucidocclist-equiv-congruence-on-x
 (implies (vl-lucidocclist-equiv x x-equiv)
          (equal (vl-lucid-collect-resolved-slices x)
                 (vl-lucid-collect-resolved-slices x-equiv)))
 :rule-classes :congruence)