Idris2Doc : System.File.ReadWrite

System.File.ReadWrite

fEOF : HasIO io => File -> io Bool

Totality: total

fGetChar : HasIO io => File -> io (Either FileError Char)

Totality: total

fGetChars : HasIO io => File -> Int -> io (Either FileError String)

Totality: total

fGetLine : HasIO io => File -> io (Either FileError String)

Totality: total

fPutStr : HasIO io => File -> String -> io (Either FileError ())

Totality: total

fPutStrLn : HasIO io => File -> String -> io (Either FileError ())

Totality: total

fSeekLine : HasIO io => File -> io (Either FileError ())

  Seek through the next newline.
  This is @fGetLine@ without the overhead of copying
  any characters.

Totality: total

readFile : HasIO io => String -> io (Either FileError String)

readFilePage : HasIO io => Nat -> Fuel -> String -> io (Either FileError (Bool, List String))

  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 : HasIO io => String -> io (Either FileError ())

Totality: total

writeFile : HasIO io => String -> String -> io (Either FileError ())

  Write a string to a file

Totality: total