		Search-engine friendly clone of the ACL2 documentation.

Vl-printedlist-p

Vl-printedlist-peek

Extract the last character that was printed.

Signature
(vl-printedlist-peek x) → maybe-char
Arguments: x — The printed list, which we assume is in reverse order!.
Guard (vl-printedlist-p x).
Returns: maybe-char — Type (or (not maybe-char) (characterp maybe-char)).

This is generally useful for things like insert a space unless we just printed a newline, etc.

Definitions and Theorems

Function: vl-printedlist-peek

(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: return-type-of-vl-printedlist-peek

(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)