		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-print-eliminated-descs

Signature
(vl-print-eliminated-descs final orig &key (ps 'ps)) → ps
Arguments: final — final design.
Guard (vl-design-p final).; orig — original design.
Guard (vl-design-p orig).

Definitions and Theorems

Function: vl-print-eliminated-descs-fn

(defun vl-print-eliminated-descs-fn (final orig ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (and (vl-design-p final)
                             (vl-design-p orig))))
 (let ((__function__ 'vl-print-eliminated-descs))
   (declare (ignorable __function__))
   (b* ((final-descs
             (mergesort (vl-descriptionlist->orignames
                             (vl-remove-nameless-descriptions
                                  (vl-design-descriptions final)))))
        (orig-descs
             (mergesort (vl-descriptionlist->orignames
                             (vl-remove-nameless-descriptions
                                  (vl-design-descriptions orig)))))
        (missing (difference orig-descs final-descs)))
     (vl-pp-stringlist-lines missing))))