Re: [isabelle] Problems with Char_ord



Hi.

The other workaround would be to check what parts of the collection
framework really depend on the product ordering (I suppose none, and
it's only there to have linorder for as many datatypes as possible, such
that usage with Red  Black Trees is possible. Then, one could think of
moving the instantiation it to an own file that is not imported by
default.

Peter


On Sa, 2012-08-25 at 07:43 -0700, Brian Huffman wrote:
> 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.