Convert a printed list (in reverse order) into characters (in proper order).
(vl-printedlist->chars x acc) → chars
Function:
(defun vl-printedlist->chars (x acc) (declare (xargs :guard (vl-printedlist-p x))) (let ((__function__ 'vl-printedlist->chars)) (declare (ignorable __function__)) (b* (((when (atom x)) acc) (x1 (vl-printed-fix (car x))) ((when (characterp x1)) (vl-printedlist->chars (cdr x) (cons x1 acc)))) (vl-printedlist->chars (cdr x) (str::append-chars x1 acc)))))
Theorem:
(defthm character-listp-of-vl-printedlist->chars (implies (character-listp acc) (b* ((chars (vl-printedlist->chars x acc))) (character-listp chars))) :rule-classes :rewrite)