<div dir="ltr"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">Ah, good.</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">Thanks, This solves my problem.<br>
</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">As a side curiosity, can the serialised type family be used to encode/decode to xml?<br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">
<br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">2014-04-14 14:16 GMT+02:00 Adam Chlipala <span dir="ltr"><<a href="mailto:adamc@csail.mit.edu" target="_blank">adamc@csail.mit.edu</a>></span>:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><u></u>
<div bgcolor="#ffffff" text="#000000"><div class="">
On 04/14/2014 03:13 AM, Marco Maggesi wrote:
<blockquote type="cite">
<div dir="ltr">I have a tree-like datatype as follows
<div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small"><br>
</div>
<div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">
<div class="gmail_default">datatype tree =</div>
<div class="gmail_default"> | Leaf of { Label : string }</div>
<div class="gmail_default"> | Node of { Label : string, Children :
list tree}</div>
<div><br>
</div>
<div>and I would like to write values of tree type inside an SQL
database.</div>
</div>
</div>
</blockquote>
<br></div>
I expect the built-in [serialized] type family is exactly what you
want. You could help me test the documentation, by seeing if this tip
is enough to point you in the right direction without more detail
here. :)<br>
</div>
</blockquote></div><br></div>