All Questions
Tagged with universe-polymorphism coq
3
questions
5
votes
1
answer
200
views
Universe polymorphism and Coq standard library
When developing in Coq with the Universe Polymorphism flag on, the standard library introduces unwelcome universe constraints because it is universe monomorphic.
Is there an alternative standard ...
- 75
4
votes
1
answer
109
views
Universe polymorphism and modules in Coq
The following code (without universe polymorphism) is accepted by Coq (8.16.0) :
...
- 175
3
votes
2
answers
223
views
Universe inconsistency errors when using ZF model in Coq
I am trying to use a formal logic system I recently implemented in Coq to study ZF set theory. In order to do this, I need to define a type representing the domain in question, and then prove that ...
- 195