Re: [isabelle] A large mutually recursive data type

Dear Victor,

> The option 1 is clearly not viable, since it would imply change all the current Cerberus code. It would be great if we could try the second option. Since I am still deciding how to proceed, I donât have firm deadlines yet.

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.



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