<div dir="ltr"><div>Philipp added the Bytes type in <a href="https://github.com/UlfNorell/agda-prelude/commit/6214370064f14b">https://github.com/UlfNorell/agda-prelude/commit/6214370064f14b</a> to do binary IO, but it doesn't look like he added any functions to create them other than reading from file.<br><br></div>/ Ulf<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Feb 25, 2018 at 10:55 AM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div>There is a Bytes Type in agda-prelude, <br><a href="https://github.com/UlfNorell/agda-prelude/blob/2e3addb9a434ed121805fa571f1dd0a077076a29/src/Prelude/Bytes.agda" target="_blank">https://github.com/UlfNorell/<wbr>agda-prelude/blob/<wbr>2e3addb9a434ed121805fa571f1dd0<wbr>a077076a29/src/Prelude/Bytes.<wbr>agda<br></a><br></div>but there is no defined way to encode/decode a builtin type to/from Bytes.<br></div></div></div>Is there a way to perform the serialization with the builtin types or do I have to define my own pragmas?<br></div>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>