an ACL2 character-based analogue of CLTL's *standard-input*
Major Section:  IO

The value of the ACL2 constant *standard-ci* is an open character input channel that is synonymous to Common Lisp's *standard-input*.

ACL2 character input from *standard-ci* is actually obtained by reading characters from the stream named by Common Lisp's *standard-input*. That is, by changing the setting of *standard-input* in raw Common Lisp you can change the source from which ACL2 reads on the channel *standard-ci*. See *standard-co*.