Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problems with Char_ord


view this post on Zulip Email Gateway (Aug 19 2022 at 08:23):

From: Manuel Eberl <eberlm@in.tum.de>
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?

Cheers,
Manuel

view this post on Zulip Email Gateway (Aug 19 2022 at 08:24):

From: Brian Huffman <huffman@in.tum.de>
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.

view this post on Zulip Email Gateway (Aug 19 2022 at 08:24):

From: Peter Lammich <lammich@in.tum.de>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 08:24):

From: Tobias Nipkow <nipkow@in.tum.de>
Am 25/08/2012 16:43, schrieb Brian Huffman:

On Fri, Aug 24, 2012 at 12:56 PM, Manuel Eberl <eberlm@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.

Done.

Tobias


Last updated: Mar 29 2024 at 04:18 UTC