Re: [isabelle] A large mutually recursive data type
> 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