Email Gateway (Aug 22 2022 at 15:48): Email Gateway (Aug 22 2022 at 15:48):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts of the algebraic type class hierarchy,
I noticed that in Isabelle2016-1, it is impossible to interpret the locale comm_monoid_set
because the theorem name "commute" is used both in abel_semigroup and comm_monoid_set,
which is a sublocale of abel_semigroup. Consequently, the command
interpretation foo: comm_monoid_set ... ...
raises the error
Duplicate fact declaration "Scratch.foo.commute" vs. "Scratch.foo.commute"
One can get around this by first interpreting abel_semigroup with the same parameters but
a different name prefix, but this is just a hack. Is it possible to rename one of the
commute lemmas before the next release to avoid the clash?
Best,
Andreas
Last updated: Apr 26 2024 at 04:17 UTC