All Questions
2
questions with no upvoted or accepted answers
2
votes
0
answers
45
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
151
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