search

MarcelineVQ / idris2-bytes

ByteStrings for Idris2!
Other
7 stars 0 forks source link

Add Strict File IO #2

Open Matthew-Mosior opened 3 years ago

Matthew-Mosior commented 3 years ago

Hi,

I'm really excited about this package as I am just jumping into the world of Idris (Idris2). I have written some code in Idris2, but would use this package's ByteString implementation (there currently isn't a ByteString implementation packaged with Idris2?), since String seems quite slow.

What are your plans for incorporating file IO operations/functions for this package?

Thanks!!

Matthew-Mosior commented 3 years ago

I now see that in https://github.com/MarcelineVQ/idris2-bytes/blob/master/src/Data/Bytes/Lazy/IO.idr, there are readFile and writeFile functions, that I can then convert to strict bytestrings should I choose to. I do see that there is a toStrict function in https://github.com/MarcelineVQ/idris2-bytes/blob/master/src/Data/Bytes/Lazy/API.idr, but I see that there is hole in the rhs?