Re: [isabelle] Proof failed for datatype



Dear Corey,

> As far as I can tell, I seem to have run into an issue with the datatype 
> package. After slightly increasing the complexity of an existing 
> datatype I get a 'Proof failed' error message.
> 
> The problematic datatype is
> datatype ('s, 'p) test' =
>    Test' "(('s, 'p) test' à 's set à 's set) list"

The bug appears to be already fixed in the development version of Isabelle, and hence in the forthcoming release (expected before the end of the year). There should be easy (but ugly) workarounds, e.g. by using a type isomorphic to Ã. Let me know if you want a patch for Isabelle2016.

Cheers,

Jasmin





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