krauss at in.tum.de
Wed Jan 21 09:43:15 CET 2009
Amine Chaieb wrote:
> If typerep is mainly used in connection with code-generation (as I
> understand) isn't it an option to generate all these instances when you
> call any code-generation facility? Or even in prior step e.g. called
That would make the problem worse: You would then be unable to merge two
theories that independently called, say value [code] for the first time.
> Besides, I don't object to the idea of typerep at all, I am just
> confused why the names clash? (Wasn't this the problem).
The problem is caused that two independent (though identical) instances
of the typerep class are generated automatically in different branches.
It seems there is no way of avoiding this in general.
For Gerwins undergrad students it should not happen though, since they
only start at official entry points and reboot frequently :-)
More information about the isabelle-dev