		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-jp-reportcard-aux

Signature
(vl-jp-reportcard-aux x &key no-html (ps 'ps)) → ps
Arguments: x — Guard (vl-reportcard-p x).; no-html — Guard (booleanp no-html).

Definitions and Theorems

Function: vl-jp-reportcard-aux-fn

(defun vl-jp-reportcard-aux-fn (x no-html ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (and (vl-reportcard-p x)
                              (booleanp no-html))))
  (let ((__function__ 'vl-jp-reportcard-aux))
    (declare (ignorable __function__))
    (b* (((when (atom x)) ps)
         ((cons modname warnings) (car x))
         (modname (if (eq modname :design)
                      "Design Root"
                    modname)))
      (vl-ps-seq (vl-indent 1)
                 (jp-str modname)
                 (vl-print ":")
                 (vl-jp-warninglist warnings
                                    :no-html no-html)
                 (if (atom (cdr x)) ps (vl-println ","))
                 (vl-jp-reportcard-aux (cdr x)
                                       :no-html no-html)))))