[isabelle-dev] Issues with "interpretations"

[Jasmin Blanchette]

Hi Andreas,

> > 4. If anybody has any ideas on how to address Scenario 3, please let me know!
> I don't think that scenario 3 is the one to address. IMO the hooks should behave as if they were executed in the name space of the datatype declaration, so size is doing something sensible already.

In a way, you're right. Scenario 3 isn't a scenario at all, it's really just a tentative solution to Scenario 2.

> Rather do I think that it seems worthwhile to address scenario 2 by making name space merges more liberal. If there is a duplicate declaration of a constant, one could check whether the declarations of the constants are equivalent, and accept if so. Since I am not familiar with the internals, I do not know whether such a change is feasible in the current implementation.

Even if this could be achieved with little code, this sounds scaringly hackish...

Jasmin