Questions tagged [module]

Module generally refers to a logical subdivision of the whole program.

Filter by
Sorted by
Tagged with
1 vote
1 answer

What is the correct way to define a DecidableType module?

I have this type in Coq: Inductive s_symb : Type := | s_symb_expr : nat -> s_symb | s_symb_fld : nat -> list string -> s_symb. I want to create a ...
Pietro Braione's user avatar
3 votes
1 answer

Universe polymorphism and modules in Coq

The following code (without universe polymorphism) is accepted by Coq (8.16.0) : ...
Dave's user avatar
  • 133
7 votes
1 answer

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 ...
Ende Jin's user avatar
  • 429
6 votes
1 answer

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 ...
Ende Jin's user avatar
  • 429