an ACL2 object-based analogue of CLTL's *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*.