Brian Huffman wrote: > I, for one, am rather alarmed at the hurdles that Amine was forced to > overcome to do a simple merge of two theories.
I agree. > I think that the automatic class-instantiations should be disabled > immediately, and replaced with a new top-level command so that these > instantiations can be done explicitly, and individually. In fact, "typerep" is not the only class that is instantiated automatically. Another one is "size", which is also of a technical nature. But it never posed problems, I think, because it is installed early enough that everybody inherits from it. I think that automatic class instantiations are acceptable provided that a) the class is for "internal" use of some tools and manual instantiation is discouraged, and b) The mechanism is installed early enough to avoid the merge issue. IMO the options are 1) Make the whole Typerep theory optional, to be loaded together with the Imperative HOL theories. 2) Typerep provides a top-level command for generating the instantiations. 3) Move Typerep up the hierarchy, such that it is always present and there are no merge problems. Note that 1 and 2 do not actually solve the problem but only limit it to theories that use Imperative HOL (in 1) or the top-level command (in 2). I think I nevertheless prefer option 1, since Typerep is really a specialized thing. The cleanest, but also the hardest solution would be to make class instances "applicative" instead of "generative" (I may be streching the terms a bit far here), such that equal class instances do *not* collide at a later merge. Alex
