Idris2Doc : System.File.Buffer

System.File.Buffer

createBufferFromFile : HasIOio => String -> io (EitherFileErrorBuffer)
  Create a new buffer by opening a file and reading its contents into a new
buffer whose size matches the file size.

@ fn the name of the file to read

Totality: total
readBufferData : HasIOio => File -> Buffer -> Int -> Int -> io (EitherFileError ())
  Read the data from the file into the given buffer.

@ fh the file handle to read from
@ buf the buffer to read the data into
@ offset the position in buffer to start adding
@ maxbytes the maximum size to read; must not exceed buffer length

Totality: total
writeBufferData : HasIOio => File -> Buffer -> Int -> Int -> io (EitherFileError ())
  Write the data from the buffer to the given `File`.
(If you do not have a `File` and just want to write to a file at a known
path, you probably want to use `writeBufferToFile`.)

@ fh the file handle to write to
@ buf the buffer from which to get the data to write
@ offset the position in buffer to write from
@ maxbytes the maximum size to write; must not exceed buffer length

Totality: total
writeBufferToFile : HasIOio => String -> Buffer -> Int -> io (EitherFileError ())
  Attempt to write the data from the buffer to the file at the specified file
name.

@ fn the file name to write to
@ buf the buffer from which to get the data to write
@ max the maximum size to write; must not exceed buffer length

Totality: total