All Questions
Tagged with universe-polymorphism coq
3
questions
3
votes
2
answers
222
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
5
votes
1
answer
196
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
108
views
Universe polymorphism and modules in Coq
The following code (without universe polymorphism) is accepted by Coq (8.16.0) :
...
- 175