coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Namespace Modules inside Sections

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Namespace Modules inside Sections
Date: Sat, 26 May 2018 22:25:44 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f181.google.com
Ironport-phdr: 9a23:xW3vAxL00UlrR7r07tmcpTZWNBhigK39O0sv0rFitYgRI/vxwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhygHOTA382/Zl9J+g75ArR27uxBy2ZTZbJ2JOPd8eK7WYNMURXBGXsZUTyFMHpizb4sOD+oaPeZXsYr9rEYSoBu4HwasAv7gwSJPi3DsxqI60+UhERrG3AM+HNICqm7brNPvO6cUTO+51qjIzTTfb/NZwjr9543IfQogofGIR75/bc3RyUw2Gg7Dk16ep4vlPzaP2eQMtWiW9/ZvVeW1i24htQ5xpjyvyt0yhYbUm4IYzE3P+yZhwIstO9G0VEp2bcSnHZZQrS2WKop7Tt44T211uys217sLsoOhcicQ0pQo3RvfZuSHc4eW5hLjU/6cITJii3JkfLKznhaz8Ea8xuHlWMm4zVVHojdfntnDsXAN0BPT6syZRfdn4kih3jOP2xjS6uFCP080ibLWJ4A9zrM0jJYeskTOEjXrlEj3kaOabFgo9+u15+j/Z7XpvJ6cN4t6igHkNaQun9SyDv4jPQgOXmib4uS826Pg/UHjWrpKiOc5kq/Ev5zAJMQbp7K5AwBO34Ys7hawFTam0NACkXYbK1JFfQqLj5L1NFHWPPD4EfC/jkywnzds3vDKJ6HuApHQLnfYi7rhZrZ860tEyAUp19xf5pRUCqsAIP3pQEPxusbYXVcFNFm/xP+iA9Fg3MtKUmWWR6SdLan6sFmS5+tpLfPaN6EPvzOoAvIl5uXugHxxsFkUe6XhiZIdaHGjHvllZUyfaHzgxNYADWgisQ83Teisg1qHB20AL02uVr4xs2loQLmtCp3OE9j00e6xmRyjF5gTXVhoT1WFEHPmbYKBAq5eZyebI8snmTsBB+H4F90RkCq2vQq/8IJJa/LO83RB553m3dlxoebUkENqrGEmP4Gmy2iIClpMsCYISjsxhv4tpEV8zhKSzvA9jaUITJpc4PRGVgp8PpnZnbR3

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