ModuleSystem

Module System

• Introduction to modules through a ModuleSystemTutorial_.

• ModulesForTheories_: Using modules and records to capture mathematical theories.

• RecordsNotModules_: Why you shouldn't use the module system at all, and use dependent records instead.

• ModulesNotRecords_: Why the previous line does not always stand.

• ProofTermsConsideredHarmful_: Why using dependent records can be difficult, and sometimes inadvisable.

• TypeClasses_ (experimental in Coq 8.2) can also be used to capture mathematical theories, like in IsabelleTheoremProver_. They use parameterized dependent records internally.

• ModulesBibliography_: Various pointers to modules in systems like Coq.

• OpenIssuesWithModules_: A discussion on various issues about Coq module system and how to address them.

.. ############################################################################

.. _ModuleSystemTutorial: ../ModuleSystemTutorial

.. _ModulesForTheories: ../ModulesForTheories

.. _RecordsNotModules: ../RecordsNotModules

.. _ModulesNotRecords: ../ModulesNotRecords

.. _ProofTermsConsideredHarmful: ../ProofTermsConsideredHarmful

.. _TypeClasses: ../TypeClasses

.. _IsabelleTheoremProver: ../IsabelleTheoremProver

.. _ModulesBibliography: ../ModulesBibliography

.. _OpenIssuesWithModules: ../OpenIssuesWithModules