Re: [isabelle] Problem with quickcheck in Isabelle2015
Dear Lars, Thomas,
> the "datatype" command has been replaced with a newer implementation since
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