Inspect the next character that will be read from an open
Signature: (peek-char$ channel state-state) returns
This is a logic-mode function, but its logical definition is tricky; see logical-story-of-io.
Under the hood, this uses Lisp's I/O functions to say which character will be retrieved next by read-char$, without altering the contents of the stream. This provides only a single character of lookahead.
You should typically never need to reason about
(defthm peek-char$-removal (equal (peek-char$ channel state) (mv-nth 0 (read-char$ channel state))))