[Agda] Serialization to ByteString

[Ulf Norell]

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.

/ Ulf

On Sun, Feb 25, 2018 at 10:55 AM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> There is a Bytes Type in agda-prelude,
> https://github.com/UlfNorell/agda-prelude/blob/
> 2e3addb9a434ed121805fa571f1dd0a077076a29/src/Prelude/Bytes.agda
>
> 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
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180225/a37965c6/attachment.html>