		Search-engine friendly clone of the ACL2 documentation.

Delayredux

Vl-modulelist-delayredux

Signature
(vl-modulelist-delayredux x &key vecp state-onlyp) → new-x
Arguments: x — Guard (vl-modulelist-p x).
Returns: new-x — Type (vl-modulelist-p new-x), given the guard.

Definitions and Theorems

Function: vl-modulelist-delayredux-fn

(defun vl-modulelist-delayredux-fn (x vecp state-onlyp)
 (declare (xargs :guard (vl-modulelist-p x)))
 (let ((__function__ 'vl-modulelist-delayredux))
  (declare (ignorable __function__))
  (b* (((mv x-prime addmods)
        (vl-modulelist-delayredux-aux x
                                      :vecp vecp
                                      :state-onlyp state-onlyp))
       (merged (union (mergesort x-prime)
                      (mergesort addmods)))
       ((unless (uniquep (vl-modulelist->names merged)))
        (raise "Name collision for ~&0."
               (duplicated-members (vl-modulelist->names merged)))))
    merged)))

Theorem: vl-modulelist-p-of-vl-modulelist-delayredux

(defthm vl-modulelist-p-of-vl-modulelist-delayredux
 (implies
      (and (force (vl-modulelist-p x)))
      (b* ((new-x (vl-modulelist-delayredux-fn x vecp state-onlyp)))
        (vl-modulelist-p new-x)))
 :rule-classes :rewrite)

Theorem: no-duplicatesp-equal-of-vl-modulelist->names-of-vl-modulelist-delayredux

(defthm
 no-duplicatesp-equal-of-vl-modulelist->names-of-vl-modulelist-delayredux
 (no-duplicatesp-equal
      (vl-modulelist->names
           (vl-modulelist-delayredux x
                                     :vecp vecp
                                     :state-onlyp state-onlyp))))