Re: [isabelle] primcorec complains about invalid map function



Am 07.02.2014 um 12:11 schrieb Johannes Hölzl <hoelzl at in.tum.de>:

> 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)

Sure, you guys do what you want. ;)

But the "DUP" is a general issue, and we had to address it.

For the record: A "DUP" exception might still arise in odd cases where two theories independently register ctr sugar for the same type in a different way and then merge. Perhaps we should simply do like others do, namely "Symtab.merge (K true)", in which case the "canonical" order of imports decides who wins.

This is one reason why I'm slightly attacted to the possibility of having several ctr sugar records. On the other hand, some applications might not be able to cope with this gracefully and will have to pick a winner anyway...

Jasmin





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