All Questions
6
questions
2
votes
0
answers
44
views
A module signature is silently changed when it is imported. Its `eq_dec` lemma has its `=` operator changed to `eq` and no longer works
This following works as I'd expect it to. But if I place the TypeDef_S signature in another file then the apply typeDef.eq_dec. ...
- 75
2
votes
1
answer
150
views
Is there a way to rename parameters when including/reusing a module type in Coq?
Say I have a (more general) module type Collection that specifies some operations like read and write and now I want to create (more specialized) module types like <...
- 121
2
votes
1
answer
81
views
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 ...
- 282
4
votes
1
answer
108
views
Universe polymorphism and modules in Coq
The following code (without universe polymorphism) is accepted by Coq (8.16.0) :
...
- 175
7
votes
1
answer
108
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
154
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