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
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 :
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