*STANDARD-CI*
an ACL2 character-based analogue of CLTL's *standard-input*
Major Section: PROGRAMMING
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*.
