@@ -156,9 +156,12 @@ file management follows a resource usage protocol with the following
156These requirements can be expressed formally by creating a
156These requirements can be expressed formally by creating a
157``FILE_IO`` effect parameterised over a file handle state, which is
157``FILE_IO`` effect parameterised over a file handle state, which is
158either empty, open for reading, or open for writing. The ``FILE_IO``
158either empty, open for reading, or open for writing. The ``FILE_IO``
159−effect’s definition is given below. Note that this
159+effect’s definition is given below.
160−effect is mainly for illustrative purposes—typically we would also like
162+ This effect is mainly for illustrative purposes.
163+ Typically we would also like to support random access files and
161−to support random access files and better reporting of error conditions.
164+ better reporting of error conditions.
163.. code-block:: idris
166.. code-block:: idris