Re: [isabelle] "Clash of specification" error



Hi Dominic,

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.

Best,
Andreas

On 17/11/16 16:22, Dominic Mulligan via Cl-isabelle-users wrote:
Hi,

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
dependencies:

Clash of specifications for less:
  "List_lexord.ord_list_inst.less_list_def"â
  "Prefix_Order.ord_list_inst.less_list_def"â

Minimum example:

theory
  Error_Monad
imports
  Main
  "$AFP/Word_Lib/Word_Enum"
  "~~/src/HOL/Library/List_lexord"
begin

(* XXX *)

end


(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?

Thanks,
Dominic





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.