Re: [isabelle] Proof failed for datatype



Dear Corey,

> On 15 Sep 2016, at 12:35, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
> 
> 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.

another (much simpler) workaround is to put a âdeadâ annotation on âs (it is dead anyway since it occurs as a parameter to set):

datatype (dead 's, 'p) test' =
   Test' "(('s, 'p) test' à 's set à 's set) listâ

Cheers,
Dmitriy



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