*standard-input*
Major Section: PROGRAMMING
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*.