Stream: General

Topic: Theory namespaces


view this post on Zulip Josh Chen (Jul 31 2020 at 09:07):

If session B imports session A which has theory My_Theory, I would expect to be able to create a new theory file with the same name in B, and have both A.My_Theory and B.My_Theory disambiguated by session namespace business. This doesn't seem to be the case?...

Relevant mailing list links:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2020-March/msg00001.html
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-January/msg00003.html

Still not fixed since 2011, I see.

view this post on Zulip Josh Chen (Jul 31 2020 at 09:12):

I found the answer on the mailing list after I wrote the first post (which, as so many other things, seems to be just "it can't be done"...), but I'll leave this up here for newcomers.

view this post on Zulip Mathias Fleury (Jul 31 2020 at 11:42):

This is one reason why the AFP contains a Multiset_More, a Missing_Multiset, a Missing_Multiset2, a multisets_continued (sic), and a Multiset_Extension: You want a new name each time


Last updated: Mar 28 2024 at 20:16 UTC