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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
