@@ -117,9 +117,10 @@ FILE_IO t = MkEff t FileIO
117||| @ m The file mode.
117||| @ m The file mode.
118open : (fname : String)
118open : (fname : String)
119 -> (m : Mode)
119 -> (m : Mode)
120+ -> { [FILE_IO ()] ==> {result}
120− -> { [FILE_IO ()] ==> [FILE_IO (if result
121+ [FILE_IO (if result
121− then OpenFile m
122+ then OpenFile m
122− else ())] } Eff Bool
123+ else ())] } Eff Bool
123open f m = call $ Open f m
124open f m = call $ Open f m