*standard-input*
Major Section: IO
The value of the ACL2 constant *standard-oi* is an open object input
channel that is synonymous to Common Lisp's *standard-input*.
ACL2 object input from *standard-oi* is actually obtained by reading
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-oi*. See *standard-co*.
