Stream: Coq users

Topic: Namespaces


view this post on Zulip Gregory Malecha (Sep 17 2021 at 19:23):

Someone pointed out the CEP on namespaces (https://github.com/coq/ceps/pull/25/files) to me today and I was pretty interested. It seems like namespaces are orthogonal to modules and I'm wondering if there is something that forces that to be the case, or if it is historical. I have never seen a module system that allows modules to be extended after-the-fact, but I can't come up with something that would go wrong if that were the case.


Last updated: Jan 31 2023 at 14:03 UTC