Re: [isabelle] Problem with quickcheck in Isabelle2015

Dear Lars, Thomas,

> the "datatype" command has been replaced with a newer implementation since
> Isabelle2012.

I guess Lars meant Isabelle2015.

> That replacement also meant reimplementation of the old
> facilities. Unfortunately, not everything was/could be implemented. I've
> stumbled over the same problem before*: Quickcheck generators will only be
> installed for datatypes without nested recursion.

This is unfortunate. Having done the transition myself, I didn't realized I introduced this limitation (and the conversation between Andreas and Lars didn't wake me up). I will look into this.



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