Re: [isabelle] primcorec complains about invalid map function



Am Freitag, den 07.02.2014, 10:30 +0100 schrieb Jasmin Blanchette:
> > Happy debugging,
> 
> Ah, I can already see what's going on: "Coinductive_Nat" redefines the "Ctr_Sugar" entry for "nat", whereas "Probability" doesn't. Merge then has to choose between two different entries and can't make up its mind.

Hm, in this particular case the fix is to move most parts of
Coinductive_Nat to HOL/Library/Extended_Nat. I think we should even
change the definition of enat to use codatatype enat = eZero | eSuc
(epred: enat)


 - Johannes

PS: This could be another nice (in the sky) feature for (co)datatype:

 codatatype enat = (0::zero) | eSuc (epred: enat)

and automatically have all your rules etc about 0 instead of Zero :-)
Of course this would only work for syntactic typeclasses.








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