@@ -3,7 +3,7 @@ module Data.Buffer
33%include C "idris_buffer.h"
44
55||| A buffer is a pointer to a sized, unstructured, mutable chunk of memory.
6−||| There are primitive operations for gettng and setting bytes, ints (32 bit)
6+||| There are primitive operations for getting and setting bytes, ints (32 bit)
77||| and strings at a location in the buffer. These operations silently fail
88||| if the location is out of bounds, so bounds checking should be done in
99||| advance.
@@ -133,7 +133,7 @@ readBufferFromFile (FHandle h) buf max
133133 pure (record { location $= (+numread) } buf)
134134
135135||| Write 'maxbytes' from the buffer from a file, returning a new
136−||| buffer with the 'locaton' pointer moved along
136+||| buffer with the 'location' pointer moved along
137137export
138138writeBufferToFile : File -> Buffer -> (maxbytes : Int) -> IO Buffer
139139writeBufferToFile (FHandle h) buf max