Re: [isabelle] A large mutually recursive data type

Dear Victor,

I wrote:

> The lack of scalability of the "(co)datatype" package in terms of mutual recursion has been an annoyance for many years. I believe we have 80% or 90% of the work done towards a scalable solution, thanks to the nested-to-mutual reduction I mentioned in my previous email.
> I hope to be able to come back to you in the next weeks with some good news.

Dmitriy and I have made some progress on this front, and things look promising, but it might still take two or three weeks before we can push something to Isabelle.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.