		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-comma-sep

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

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

Definitions and Theorems

Function: pprint-comma-sep

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

Theorem: msgp-of-pprint-comma-sep

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