@@ -153,7 +153,7 @@ file management follows a resource usage protocol with the following
153153
154154- When a file is closed, its handle should no longer be used
155155
156−These requirements can be expressed formally in , by creating a
156+These requirements can be expressed formally by creating a
157157``FILE_IO`` effect parameterised over a file handle state, which is
158158either empty, open for reading, or open for writing. The ``FILE_IO``
159159effect’s definition is given below. Note that this
@@ -173,7 +173,7 @@ to support random access files and better reporting of error conditions.
173173
174174 open : (fname : String)
175175 -> (m : Mode)
176− -> Eff Bool [FILE_IO ()]
176+ -> Eff Bool [FILE_IO ()]
177177 (\res => [FILE_IO (case res of
178178 True => OpenFile m
179179 False => ())])
@@ -191,7 +191,7 @@ In particular, consider the type of ``open``:
191191
192192 open : (fname : String)
193193 -> (m : Mode)
194− -> Eff Bool [FILE_IO ()]
194+ -> Eff Bool [FILE_IO ()]
195195 (\res => [FILE_IO (case res of
196196 True => OpenFile m
197197 False => ())])
@@ -207,7 +207,7 @@ we continue the protocol accordingly.
207207
208208 readFile : Eff (List String) [FILE_IO (OpenFile Read)]
209209 readFile = readAcc [] where
210− readAcc : List String -> Eff (List String) [FILE_IO (OpenFile Read)]
210+ readAcc : List String -> Eff (List String) [FILE_IO (OpenFile Read)]
211211 readAcc acc = if (not !eof)
212212 then readAcc (!readLine :: acc)
213213 else pure (reverse acc)