		Search-engine friendly clone of the ACL2 documentation.

Tty-bufferp

Recognizer for the TTY buffers.

Signature
(tty-bufferp x) → *

tty-bufferp recognizes buffers which are valid as the tty-in and tty-out fields of the x86 stobj. These are true-listps which only contain 8-bit unsigned integers.

Definitions and Theorems

Function: tty-bufferp

(defun tty-bufferp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'tty-bufferp))
    (declare (ignorable __function__))
    (or (null x)
        (and (consp x)
             (unsigned-byte-p 8 (car x))
             (tty-bufferp (cdr x))))))