Input and Output

Presently, input and output can only be done with respect to the current input and output streams. These can be set, reset or checked using the file handling predicates described below. The default input and output streams are internally denoted by userin and userout (the user accesses them both via the name ``user'', and they refer to the user's terminal).