I could use haskell' Binary library, but that would require me to know the
haskell type of the builtin types.
The other option is that Agda has primitive functions that make the
transformation, this way I do not need to know how builtin types are
represented in Haskell.
The other option is to define my my own pragmas for the builtin types. I do
not want to do that because the builtin representation was done for a
I would prefer the second option. To add primitive functions that make the
Philipp added the Bytes type in https://github.com/UlfNorell/
agda-prelude/commit/6214370064f14b to do binary IO, but it doesn't look
like he added any functions to create them other than reading from file.
On Sun, Feb 25, 2018 at 10:55 AM, Apostolis Xekoukoulotakis <
Post by Apostolis Xekoukoulotakis
There is a Bytes Type in agda-prelude,
but there is no defined way to encode/decode a builtin type to/from Bytes.
Is there a way to perform the serialization with the builtin types or do
I have to define my own pragmas?
Agda mailing list