Idris2Doc : System.File.ReadWrite


appendFile : HasIOio => String -> String -> io (EitherFileError ())
  Append the given string to the file at the specified name. Opens the file in
with the `Append` mode.

@ filePath the file to write to
@ contents the string to write to the file

Totality: total
fEOF : HasIOio => File -> ioBool
  Check whether the end-of-file indicator for the given file handle is set.

@ h the file handle to check

Totality: total
fGetChar : HasIOio => File -> io (EitherFileErrorChar)
  Get the next character from the given file handle.

@ h the file handle to read from

Totality: total
fGetChars : HasIOio => File -> Int -> io (EitherFileErrorString)
  Get a number of characters from the given file handle.

@ h the file handle to read from
@ max the number of characters to read

Totality: total
fGetLine : HasIOio => File -> io (EitherFileErrorString)
  Get the next line from the given file handle, returning the empty string if
nothing was read.

@ h the file handle to get the line from

Totality: total
fPutStr : HasIOio => File -> String -> io (EitherFileError ())
  Write the given string to the file handle.

@ h the file handle to write to
@ str the string to write

Totality: total
fPutStrLn : HasIOio => File -> String -> io (EitherFileError ())
  Write the given string, followed by a newline, to the file handle.

@ fh the file handle to write to
@ str the string to write

Totality: total
fRead : HasIOio => File -> io (EitherFileErrorString)
  Read all the remaining contents of a file handle

fSeekLine : HasIOio => File -> io (EitherFileError ())
  Seek through the next newline.
This is @fGetLine@ without the overhead of copying
any characters.

@ h the file handle to seek through

Totality: total
readFile : HasIOio => String -> io (EitherFileErrorString)
  Read the entire file at the given name. This function is `partial` since
there is no guarantee that the given file isn't infinite.

@ fname the name of the file to read

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.

@ offset the offset to start reading at
@ until the `Fuel` limiting how far we can read
@ fname the name of the file to read

Totality: total
removeFile : HasIOio => String -> io (EitherFileError ())
  Delete the file at the given name.

@ fname the file to delete

Totality: total
writeFile : HasIOio => String -> String -> io (EitherFileError ())
  Write the given string to the file at the specified name. Opens the file
with the `WriteTruncate` mode.
(If you have a file handle (a `File`), you may be looking for `fPutStr`.)

@ filePath the file to write to
@ contents the string to write to the file

Totality: total