		Search-engine friendly clone of the ACL2 documentation.

Std/io/write-byte$

Write one byte to an open :byte output stream.

Signature: (write-byte$ x channel state-state) returns state.

byte must be a natural number with byte < 256.
channel is a symbol that must refer to an open :byte input channel; see open-input-channel.
state is the ACL2 state.

This is a logic-mode function, but its logical definition is tricky; see logical-story-of-io. The main logical consequence is the updating of state.

Under the hood, we write a byte to the Lisp output stream that is associated with channel.

Definitions and Theorems

Theorem: state-p1-of-write-byte$

(defthm state-p1-of-write-byte$
        (implies (and (state-p1 state)
                      (symbolp channel)
                      (natp byte)
                      (< byte 256)
                      (open-output-channel-p1 channel
                                              :byte state))
                 (state-p1 (write-byte$ byte channel state))))

Theorem: open-output-channel-p1-of-write-byte$

(defthm
 open-output-channel-p1-of-write-byte$
 (implies
   (and (state-p1 state)
        (open-output-channel-p1 channel
                                :byte state))
   (open-output-channel-p1 channel
                           :byte (write-byte$ byte channel state))))