Re: [isabelle] A large mutually recursive data type
- To: Victor Gomes <vb358 at cam.ac.uk>
- Subject: Re: [isabelle] A large mutually recursive data type
- From: Jasmin Blanchette <jasmin.blanchette at inria.fr>
- Date: Sun, 3 Apr 2016 23:06:45 +0200
- Cc: Peter Sewell <Peter.Sewell at cl.cam.ac.uk>, Dmitriy Traytel <traytel at inf.ethz.ch>, Isabelle Users <cl-isabelle-users at lists.cam.ac.uk>
- In-reply-to: <C388B3D1-7DD1-4F35-95C3-66937BF1A692@inria.fr>
- References: <9EA07F44-212D-4E74-9085-D2C90E4BFD0C@cam.ac.uk> <7B624798-A387-44B8-817E-ABC7ABA8CC67@inf.ethz.ch> <204CD2AE-DA00-4512-AB7F-AA3D8F70C284@cam.ac.uk> <A3CA0D55-C9A7-47E6-A0C3-36D765BCEDA4@inria.fr> <07805EC8-4D2F-4C48-9D3E-4D6A4C21D021@cam.ac.uk> <C388B3D1-7DD1-4F35-95C3-66937BF1A692@inria.fr>
> 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