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