		Search-engine friendly clone of the ACL2 documentation.

Write-tty

Write a byte to the TTY.

Signature
(write-tty c x86) → x86
Returns: x86 — Type (x86p x86), given (x86p x86).

This function writes a byte to the tty-out field of the x86 state by consing the byte to the front of it. Including tty-raw.lsp in raw lisp smashes this function to write to a TCP port instead.

Definitions and Theorems

Function: write-tty

(defun write-tty (c x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 8) c))
  (let ((__function__ 'write-tty))
    (declare (ignorable __function__))
    (!tty-out (cons c (tty-out x86)) x86)))

Theorem: x86p-of-write-tty

(defthm x86p-of-write-tty
  (implies (x86p x86)
           (b* ((x86 (write-tty c x86)))
             (x86p x86)))
  :rule-classes :rewrite)