		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jchars

Lift print-jchar to lists.

Signature
(print-jchars chars) → part
Arguments: chars — Guard (character-listp chars).
Returns: part — Type (msgp part).

The representations of the characters are juxtaposed one after the other. This is used only for string literals, not character literals.

Definitions and Theorems

Function: print-jchars

(defun print-jchars (chars)
  (declare (xargs :guard (character-listp chars)))
  (let ((__function__ 'print-jchars))
    (declare (ignorable __function__))
    (cond ((endp chars) "")
          (t (msg "~@0~@1" (print-jchar (car chars))
                  (print-jchars (cdr chars)))))))

Theorem: msgp-of-print-jchars

(defthm msgp-of-print-jchars
  (b* ((part (print-jchars chars)))
    (msgp part))
  :rule-classes :rewrite)