		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-pp-merged-index-list

Signature
(vl-pp-merged-index-list x &key (ps 'ps)) → ps
Arguments: x — Guard (vl-merged-index-list-p x).

Definitions and Theorems

Function: vl-pp-merged-index-list-fn

(defun vl-pp-merged-index-list-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (vl-merged-index-list-p x)))
  (let ((__function__ 'vl-pp-merged-index-list))
    (declare (ignorable __function__))
    (if (atom x)
        ps
      (vl-ps-seq (vl-pp-merged-index (car x))
                 (if (consp (cdr x))
                     (if (consp (cddr x))
                         (vl-print ", ")
                       (vl-print " and "))
                   ps)
                 (vl-pp-merged-index-list (cdr x))))))