*standard-ci*
An ACL2 character-based analogue of CLTL's *standard-input*
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*.
