Re: Functions from datasorts to datasorts

2018-04-09 Thread Andrew Knapp
My one example, serialization of nested records from a tlist of @(string,t0ype), turned out to not need append. Anyhow, that's blocked for now, since I don't think you can reflect a template-argument string literal to the value level. But more generally, a convenient way to write functions

Re: Functions from datasorts to datasorts

2018-04-09 Thread Artyom Shalkhakov
2018-04-09 11:35 GMT+06:00 Andrew Knapp : > Is it possible to write (proof) functions from datasorts to datasorts? For > example, if we have > > datasort tlist = > | tnil > | tcons(t0ype, tlist) > > it would be nice to write something equivalent to > > tlist_append :

Re: Functions from datasorts to datasorts

2018-04-08 Thread gmhwxi
Could you show an example of intended use of tlist_append? On Monday, April 9, 2018 at 1:35:44 AM UTC-4, Andrew Knapp wrote: > > Is it possible to write (proof) functions from datasorts to datasorts? For > example, if we have > > datasort tlist = > | tnil > | tcons(t0ype, tlist) > > it would