nipkow at in.tum.de
Wed Jan 21 08:01:01 CET 2009
Now that I'm beginning to understand what typerep is, I most certainly
agree that it is too specialized to force it on everybody.
Alexander Krauss wrote:
> 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.
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev