I have finished the practices of
sf/lf and part of
To learn Coq’s module system, I read the following resources:
First is the official doc, it’s all about definition of abstract noun and formulas, and tells nothing about the situation and usage. I felt helpless.
Then I go to the wiki, it start with telling me how to write my own module. but why I need to write a module for just min and max, and what is the name
Sig for? and why there is
The most important things is, I still have a lot of basic problems about Coq’s modules, but these tutorial tells nothing about them, e.g.
- How can I find a module I want? by name? by type? via google? is there a site similar to hoogle for haskell?
- How to use an existing module I found? what’s the different between Import/Require?
- What is the relationship between Module and Scope?
- How does Coq organize it’s internal modules? what is the principle?
Is there any suggestion or better resources for learning Coq’s module system?