Re: [isabelle] "Clash of specification" error
Every type class can be instantiated only once for each type. For lists, there are two
different instantiations in different theories in HOL/Library: List_lexord defines the
order on lists to be lexicographic and Prefix_Order defines the order to be by prefix.
Therefore, you cannot import both into one theory, but this happens in your example,
because Word_Lib transitively imports the theory Prefix_Order. There's no way around this.
On 17/11/16 16:22, Dominic Mulligan via Cl-isabelle-users wrote:
It seems I'm unable to use the Word_Enum theory from the AFP Word
library and List_lexord theory from the HOL Library concurrently as
Isabelle-2016 raises the following exception when processing
Clash of specifications for less:
(* XXX *)
(In my development, I'm importing List_lexord in X.thy and Word_Enum
in Y.thy with a dependency between the two.)
Is there a way around this?
This archive was generated by a fusion of
Pipermail (Mailman edition) and