		Search-engine friendly clone of the ACL2 documentation.

Std/io/peek-char$

Inspect the next character that will be read from an open :character input stream.

Signature: (peek-char$ channel state-state) returns char/nil.

channel is a symbol that must refer to an open :character 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.

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 peek-char$. We prove it returns the same thing as read-char$, so you should be able to just reason about read-char$ instead.

Definitions and Theorems

Theorem: peek-char$-removal

(defthm peek-char$-removal
  (equal (peek-char$ channel state)
         (mv-nth 0 (read-char$ channel state))))