		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-vardecllist-comma-separated

Signature
(vl-pp-vardecllist-comma-separated x &key (ps 'ps)) → ps
Arguments: x — Guard (vl-vardecllist-p x).

Definitions and Theorems

Function: vl-pp-vardecllist-comma-separated-fn

(defun vl-pp-vardecllist-comma-separated-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (vl-vardecllist-p x)))
  (let ((__function__ 'vl-pp-vardecllist-comma-separated))
    (declare (ignorable __function__))
    (b* (((when (atom x)) ps)
         (ps (vl-pp-vardecl-aux (car x)))
         ((when (atom (cdr x))) ps)
         (ps (vl-print " ,")))
      (vl-pp-vardecllist-comma-separated (cdr x)))))

Theorem: vl-pp-vardecllist-comma-separated-fn-of-vl-vardecllist-fix-x

(defthm vl-pp-vardecllist-comma-separated-fn-of-vl-vardecllist-fix-x
 (equal (vl-pp-vardecllist-comma-separated-fn (vl-vardecllist-fix x)
                                              ps)
        (vl-pp-vardecllist-comma-separated-fn x ps)))

Theorem: vl-pp-vardecllist-comma-separated-fn-vl-vardecllist-equiv-congruence-on-x

(defthm
 vl-pp-vardecllist-comma-separated-fn-vl-vardecllist-equiv-congruence-on-x
 (implies (vl-vardecllist-equiv x x-equiv)
          (equal (vl-pp-vardecllist-comma-separated-fn x ps)
                 (vl-pp-vardecllist-comma-separated-fn x-equiv ps)))
 :rule-classes :congruence)