		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-foreachstmt-loopvars

Signature
(vl-pp-foreachstmt-loopvars loopvars &key (ps 'ps)) → ps
Arguments: loopvars — Guard (vl-maybe-string-list-p loopvars).

Definitions and Theorems

Function: vl-pp-foreachstmt-loopvars-fn

(defun vl-pp-foreachstmt-loopvars-fn (loopvars ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (vl-maybe-string-list-p loopvars)))
 (let ((__function__ 'vl-pp-foreachstmt-loopvars))
  (declare (ignorable __function__))
  (b* ((loopvars (vl-maybe-string-list-fix loopvars)))
   (if (atom loopvars)
       ps
    (if (atom (car loopvars))
        (vl-ps-seq (vl-print ", ")
                   (vl-pp-foreachstmt-loopvars (cdr loopvars)))
     (vl-ps-seq
      (vl-ps-span
         "vl_id"
         (vl-print-str (vl-maybe-escape-identifier (car loopvars))))
      (vl-print ", ")
      (vl-pp-foreachstmt-loopvars (cdr loopvars))))))))

Theorem: vl-pp-foreachstmt-loopvars-fn-of-vl-maybe-string-list-fix-loopvars

(defthm
 vl-pp-foreachstmt-loopvars-fn-of-vl-maybe-string-list-fix-loopvars
 (equal
  (vl-pp-foreachstmt-loopvars-fn (vl-maybe-string-list-fix loopvars)
                                 ps)
  (vl-pp-foreachstmt-loopvars-fn loopvars ps)))

Theorem: vl-pp-foreachstmt-loopvars-fn-vl-maybe-string-list-equiv-congruence-on-loopvars

(defthm
 vl-pp-foreachstmt-loopvars-fn-vl-maybe-string-list-equiv-congruence-on-loopvars
 (implies (vl-maybe-string-list-equiv loopvars loopvars-equiv)
          (equal (vl-pp-foreachstmt-loopvars-fn loopvars ps)
                 (vl-pp-foreachstmt-loopvars-fn loopvars-equiv ps)))
 :rule-classes :congruence)