		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-pp-bits

Signature
(vl-lucid-pp-bits x &key (ps 'ps)) → ps
Arguments: x — Guard (and (integer-listp x) (setp x)).

Definitions and Theorems

Function: vl-lucid-pp-bits-fn

(defun vl-lucid-pp-bits-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (and (integer-listp x) (setp x))))
  (let ((__function__ 'vl-lucid-pp-bits))
    (declare (ignorable __function__))
    (b* ((merged (vl-merge-contiguous-indices x))
         (merged (rev merged)))
      (vl-pp-merged-index-list merged))))