		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-pp-lucid-multidrive-summary

Signature
(vl-pp-lucid-multidrive-summary occs &key (ps 'ps)) → ps
Arguments: occs — Guard (vl-lucidocclist-p occs).

Definitions and Theorems

Function: vl-pp-lucid-multidrive-summary-fn

(defun vl-pp-lucid-multidrive-summary-fn (occs ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (vl-lucidocclist-p occs)))
 (let ((__function__ 'vl-pp-lucid-multidrive-summary))
  (declare (ignorable __function__))
  (if (atom occs)
      ps
   (vl-ps-seq (vl-indent 4)
              (vl-print " - ")
              (vl-pp-ctxelement-summary
                   (vl-lucidctx->elem (vl-lucidocc->ctx (car occs)))
                   :withloc t)
              (vl-println "")
              (vl-pp-lucid-multidrive-summary (cdr occs))))))

Theorem: vl-pp-lucid-multidrive-summary-fn-of-vl-lucidocclist-fix-occs

(defthm
      vl-pp-lucid-multidrive-summary-fn-of-vl-lucidocclist-fix-occs
  (equal
       (vl-pp-lucid-multidrive-summary-fn (vl-lucidocclist-fix occs)
                                          ps)
       (vl-pp-lucid-multidrive-summary-fn occs ps)))

Theorem: vl-pp-lucid-multidrive-summary-fn-vl-lucidocclist-equiv-congruence-on-occs

(defthm
 vl-pp-lucid-multidrive-summary-fn-vl-lucidocclist-equiv-congruence-on-occs
 (implies (vl-lucidocclist-equiv occs occs-equiv)
          (equal (vl-pp-lucid-multidrive-summary-fn occs ps)
                 (vl-pp-lucid-multidrive-summary-fn occs-equiv ps)))
 :rule-classes :congruence)