		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-comma-sep

Turn zero or more parts into a single part containing the initial parts, comma-separated.

Signature
(print-comma-sep parts) → part
Arguments: parts — Guard (msg-listp parts).
Returns: part — Type (msgp part), given (msg-listp parts).

Definitions and Theorems

Function: print-comma-sep

(defun print-comma-sep (parts)
  (declare (xargs :guard (msg-listp parts)))
  (let ((__function__ 'print-comma-sep))
    (declare (ignorable __function__))
    (cond ((endp parts) "")
          ((endp (cdr parts)) (car parts))
          (t (msg "~@0, ~@1" (car parts)
                  (print-comma-sep (cdr parts)))))))

Theorem: msgp-of-print-comma-sep

(defthm msgp-of-print-comma-sep
  (implies (msg-listp parts)
           (b* ((part (print-comma-sep parts)))
             (msgp part)))
  :rule-classes :rewrite)