Idris2Doc : System.File.ReadWrite

System.File.ReadWrite

fEOF : HasIOio => File -> ioBool
Totality: total
fGetChar : HasIOio => File -> io (EitherFileErrorChar)
Totality: total
fGetChars : HasIOio => File -> Int -> io (EitherFileErrorString)
Totality: total
fGetLine : HasIOio => File -> io (EitherFileErrorString)
Totality: total
fPutStr : HasIOio => File -> String -> io (EitherFileError ())
Totality: total
fPutStrLn : HasIOio => File -> String -> io (EitherFileError ())
Totality: total
fSeekLine : HasIOio => File -> io (EitherFileError ())
  Seek through the next newline.
This is @fGetLine@ without the overhead of copying
any characters.

Totality: total
readFile : HasIOio => String -> io (EitherFileErrorString)
readFilePage : HasIOio => Nat -> Fuel -> String -> io (EitherFileError (Bool, ListString))
  Read a chunk of a file in a line-delimited fashion.
You can use this function to read an entire file
as with @readFile@ by reading until @forever@ or by
iterating through pages until hitting the end of
the file.

The @limit@ function can provide you with enough
fuel to read exactly a given number of lines.

On success, returns a tuple of whether the end of
the file was reached or not and the lines read in
from the file.

Note that each line will still have a newline
character at the end.

Important: because we are chunking by lines, this
function's totality depends on the assumption that
no single line in the input file is infinite.

Totality: total
removeFile : HasIOio => String -> io (EitherFileError ())
Totality: total
writeFile : HasIOio => String -> String -> io (EitherFileError ())
  Write a string to a file

Totality: total