Email Gateway (Aug 19 2022 at 08:23): 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
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.
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
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
- Brian
Last updated: Nov 21 2024 at 12:39 UTC