coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Namespace Modules inside Sections

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr, Abhishek Anand <abhishek.anand.iitg AT gmail.com>
Subject: Re: [Coq-Club] Namespace Modules inside Sections
Date: Sun, 27 May 2018 11:50:28 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT juno.mpi-klsb.mpg.de
Ironport-phdr: 9a23:1vWt+BXD8ci/ucOAlYqo96XVC3zV8LGtZVwlr6E/grcLSJyIuqrYYxOFt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/KlMJwgqJVrhGvqRNxzIHbYp2aOvVlc6PBft4XX3ZNUtpfWiFDBI63cosBD/AGPeZdt4Tzu0EBrR+wBQKxAO3v1zlIhnDr1qA90eQhDAfG3AM7EtILqHTUrcz5NLwcUOCu1qXIyi/Db/xP1Dr79YPGfBchofSWUrJxd8rc0VUgFwTfjlWWt4PlOzeV2v4TvGeG8uptU/+khW0/qwxpvzSiyMMhhpPUio8R0FzJ9iR0zJw6KNGkUEJ3fN+pHZVKuyyaLYd6XN0uT31ytCok17ELv4OwcjIQx5Q93RHfbuSKc4iW7RLnU+acOTV4hG9jeLK4nRqy9FCgyuzlWsm31FZKtTFKnsPJtnAV2Bzf8NWIReVl8keg3zaAyRzT5/lZLU06kafXMYMtz7oqmpcQsEnPBCD7lFnugK+TbEok++yo6+r9YrXho5+RL410ihz4MqQhgcG/BPw4MgkXU2iA9+W8z6fv/UrjQLVFlvE2iLXWsIjGJcQHoa60GxNa0oE66xqmEzim1MkYkmIcIVJeeBOHipDpNEvULPD5C/e/mVWsny1xy/DIJL2ySqnKe3PEifLqeat3w09a0gs6i95Fo9p9ALEAO/L+WQfYstXeAldtOga0wv3nBdY734UXX27JA66FP4vdtFaJ4qQkJOzaN6EPvzOoEfEh6bbMkHk20QsfYK+m9Z4PaTWjAe8gJF+WNym/yuwdGHsH61JtBNfhj0ePBGYKNiSCGpkk7zR+M7qISILKR4SjmruEhXzpG4VXI3tZERaLC3i6LtzYCcdJUzqbJ4paqhJBTaKoEtRz0Amv8RTl0PxgNOWGonRF56Km78B84qjorT939TFwCJ7HgWOQSWYym3sJAjwyx6o5pFRyjFuOg/B1

Hi,

try nesting the other way around, i.e.

Module B.
Section A.
...

The way you write it, you have a module that depends on a type parameter T,
which is not even something Coq's module system can represent...

Kind regards,
Ralf

On 27.05.2018 04:25, Abhishek Anand wrote:
> I understand that there may be some difficulty in defining the semantics of
> modules, especially arbitrary modules inside sections.
> However, many Coq users use Modules only for namespaces. Can such "dummy"
> modules be allowed inside sections?
> For example, I want the following to be accepted:
>
> Section A.
> Variable T:Type.
> Module B.
> Definition id (t:T):= t.
> End B.
> End A.
>
> In Coq 8.7 (and I guess all previous versions), I get the error "Error:
> Modules
> and Module Types are not allowed inside sections."
>
> --
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/

[Coq-Club] Namespace Modules inside Sections, Abhishek Anand, 05/27/2018
- Re: [Coq-Club] Namespace Modules inside Sections, Ralf Jung, 05/27/2018
  - RE: [Coq-Club] Namespace Modules inside Sections, Soegtrop, Michael, 05/27/2018