Print a list of zero or more characters or escape sequences usable in character constants.
(print-c-char-list cchars pstate) → new-pstate
Function:
(defun print-c-char-list (cchars pstate) (declare (xargs :guard (and (c-char-listp cchars) (pristatep pstate)))) (let ((__function__ 'print-c-char-list)) (declare (ignorable __function__)) (b* (((when (endp cchars)) (pristate-fix pstate)) (pstate (print-c-char (car cchars) pstate))) (print-c-char-list (cdr cchars) pstate))))
Theorem:
(defthm pristatep-of-print-c-char-list (b* ((new-pstate (print-c-char-list cchars pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-c-char-list-of-c-char-list-fix-cchars (equal (print-c-char-list (c-char-list-fix cchars) pstate) (print-c-char-list cchars pstate)))
Theorem:
(defthm print-c-char-list-c-char-list-equiv-congruence-on-cchars (implies (c-char-list-equiv cchars cchars-equiv) (equal (print-c-char-list cchars pstate) (print-c-char-list cchars-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-c-char-list-of-pristate-fix-pstate (equal (print-c-char-list cchars (pristate-fix pstate)) (print-c-char-list cchars pstate)))
Theorem:
(defthm print-c-char-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-c-char-list cchars pstate) (print-c-char-list cchars pstate-equiv))) :rule-classes :congruence)