		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-char-list

Pretty-print a list of characters.

Signature
(pprint-char-list chars) → part
Arguments: chars — Guard (char-listp chars).
Returns: part — Type (msgp part).

We juxtapose them one after the other.

Definitions and Theorems

Function: pprint-char-list

(defun pprint-char-list (chars)
  (declare (xargs :guard (char-listp chars)))
  (let ((__function__ 'pprint-char-list))
    (declare (ignorable __function__))
    (cond ((endp chars) "")
          (t (msg "~@0~@1" (pprint-char (car chars))
                  (pprint-char-list (cdr chars)))))))

Theorem: msgp-of-pprint-char-list

(defthm msgp-of-pprint-char-list
  (b* ((part (pprint-char-list chars)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-char-list-of-char-list-fix-chars

(defthm pprint-char-list-of-char-list-fix-chars
  (equal (pprint-char-list (char-list-fix chars))
         (pprint-char-list chars)))

Theorem: pprint-char-list-char-list-equiv-congruence-on-chars

(defthm pprint-char-list-char-list-equiv-congruence-on-chars
  (implies (char-list-equiv chars chars-equiv)
           (equal (pprint-char-list chars)
                  (pprint-char-list chars-equiv)))
  :rule-classes :congruence)