		Search-engine friendly clone of the ACL2 documentation.

Dupeinst-check

Vl-pp-dupeinst-alist

Signature
(vl-pp-dupeinst-alist x &key (ps 'ps)) → ps
Arguments: x — Guard (vl-dupeinst-alistp x).

Definitions and Theorems

Function: vl-pp-dupeinst-alist-fn

(defun vl-pp-dupeinst-alist-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (vl-dupeinst-alistp x)))
  (let ((__function__ 'vl-pp-dupeinst-alist))
    (declare (ignorable __function__))
    (b* (((when (atom x)) ps)
         ((cons key insts) (car x)))
      (vl-ps-seq (vl-print "** ")
                 (vl-pp-dupeinst-key key)
                 (vl-pp-modinstlist insts nil)
                 (vl-pp-dupeinst-alist (cdr x))))))