zhangyuanlin
commented
6 years ago My answer to the title: yes. This seems to be a part of #7. 1) it is good if you can make your current implementation on addressing "names" explicit, say in dissertation. 2) in future, it seems to be good idea to introduce "local names" and namespace (under theory). In fact, we probably cannot avoid this issue when we allow people to build well organized theories (like package in Java).
Flattening a module throws everything together in a giant soup. Entities from separate modules with the same name would end up being the same entity. We've already introduced prefixing attribute functions with sort name in the translation to cope with overloading between use of attribute names.
Should function names be prefixed/scoped by the module that introduced them? If so, should the containing library and theory name contribute to the scoping?