		Search-engine friendly clone of the ACL2 documentation.

Vl-print-strings-with-commas

Vl-print-strings-with-commas-aux

Signature
(vl-print-strings-with-commas-aux x &key (ps 'ps)) → ps
Arguments: x — Guard (string-listp x).

Definitions and Theorems

Function: vl-print-strings-with-commas-aux-fn

(defun vl-print-strings-with-commas-aux-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (string-listp x)))
 (let ((__function__ 'vl-print-strings-with-commas-aux))
  (declare (ignorable __function__))
  (cond
       ((atom x) ps)
       ((atom (cdr x))
        (vl-print-str-main (car x)))
       (t (vl-ps-seq (vl-print-str-main (car x))
                     (vl-println? ", ")
                     (vl-print-strings-with-commas-aux (cdr x)))))))

Theorem: vl-print-strings-with-commas-aux-fn-of-string-list-fix-x

(defthm vl-print-strings-with-commas-aux-fn-of-string-list-fix-x
  (equal (vl-print-strings-with-commas-aux-fn (string-list-fix x)
                                              ps)
         (vl-print-strings-with-commas-aux-fn x ps)))

Theorem: vl-print-strings-with-commas-aux-fn-string-list-equiv-congruence-on-x

(defthm
 vl-print-strings-with-commas-aux-fn-string-list-equiv-congruence-on-x
 (implies (str::string-list-equiv x x-equiv)
          (equal (vl-print-strings-with-commas-aux-fn x ps)
                 (vl-print-strings-with-commas-aux-fn x-equiv ps)))
 :rule-classes :congruence)