*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*.
