Extract the last character that was printed.
(vl-printedlist-peek x) → maybe-char
This is generally useful for things like insert a space unless we just printed a newline, etc.
Function:
(defun vl-printedlist-peek (x) (declare (xargs :guard (vl-printedlist-p x))) (let ((__function__ 'vl-printedlist-peek)) (declare (ignorable __function__)) (and (consp x) (let ((x1 (vl-printed-fix (car x)))) (if (characterp x1) x1 (let ((len (length x1))) (if (zp len) (vl-printedlist-peek (cdr x)) (char x1 (1- len)))))))))
Theorem:
(defthm return-type-of-vl-printedlist-peek (b* ((maybe-char (vl-printedlist-peek x))) (or (not maybe-char) (characterp maybe-char))) :rule-classes :type-prescription)