Re: [isabelle] Problems with Char_ord



On Fri, Aug 24, 2012 at 12:56 PM, Manuel Eberl <eberlm at in.tum.de> wrote:
> Hallo,
>
> I need a linorder on strings and imported List_lexord and Char_ord for
> that purpose. However, when Isabelle tries to process the imports
> command, I get the following error:
>
>  Clash of specifications "Misc.ord_prod_inst.less_prod_def" and
> "Product_ord.ord_prod_inst.less_prod_def" for constant
> "Orderings.ord_class.less"
>
> I suspect that this has something to do with conflicting definitions of
> product orderings. The first one seems to come from
> Library/Product_ord.thy The second one probably comes from some kind of
> file that is imported by the Collection framework, which I use - perhaps
> Collections/common/Misc.thy. But how do I fix this?

Library/Char_ord.thy imports Library/Product_ord.thy, but upon
inspection it looks like this dependency is completely unnecessary. So
probably the easiest workaround is to modify Char_ord.thy by removing
"Product_ord" from the imports.

Someone ought to make this change in the repository version as well.

- Brian





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