@@ -63,6 +63,7 @@ library:
64 module Main
64 module Main
66 import Effect.StdIO
67 import Effect.StdIO
68 hello : [STDIO] Eff ()
69 hello : [STDIO] Eff ()
@@ -71,10 +72,11 @@ library:
71 main : IO ()
72 main : IO ()
72 main = run hello
73 main = run hello
74−As usual, the entry point is ``main``. All ``main`` has to do is
75+As usual, the entry point is ``main``. All ``main`` has to do is invoke the
75−invoke the ``hello`` function which supports the ``STDIO`` effect for
76+``hello`` function which supports the ``STDIO`` effect for console I/O, and
76−console I/O, and returns the unit value. The details of the ``Eff``
77+returns the unit value. All programs using the ``Effects`` library must
78+``import Effects``. The details of the ``Eff`` type will be presented in the
77−type will be presented in the remainder of this tutorial.
79+remainder of this tutorial.
79To compile and run this program, ``Idris`` needs to be told to include
81To compile and run this program, ``Idris`` needs to be told to include
80the ``Effects`` package, using the ``-p effects`` flag (this flag is
82the ``Effects`` package, using the ``-p effects`` flag (this flag is