[isabelle-dev] typrep?

[Alexander Krauss]

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
> setup-every-thing-that-has-to-do-with-code-generation?

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

Alex