Questions tagged [module]
Module generally refers to a logical subdivision of the whole program.
3
questions
3
votes
1
answer
84
views
Universe polymorphism and modules in Coq
The following code (without universe polymorphism) is accepted by Coq (8.16.0) :
...
- 133
7
votes
1
answer
92
views
Why Coq's `Include` is designed to instantiate functor with current interactive defining module?
It is surprising for me to see that Coq can Include a functor and will instantiate it with the current interactive module.
Coq Ref Manual:
Command Include ...
- 429
6
votes
1
answer
111
views
Does Coq's Module and Functor type-check incrementally?
I am trying to search the following questions online but I failed:
When applying a functor (parametrized module), will the contents inside the functor be re-type-checked?
Will Coq's command ...
- 429