(vl-print-strings-with-commas-aux x &key (ps 'ps)) → ps
Function:
(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:
(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:
(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)