\begin{verbatim}
-- File and channel names:

stdin       =  "stdin"
stdout      =  "stdout"
stderr      =  "stderr"
stdecho     =  "stdecho"
\end{verbatim}