All Questions
Tagged with soft-question inductive-type
2
questions
6
votes
4
answers
849
views
Inductive vs. recursive definitions
In Coq there are two ways to define a new type on an inductive type: Using Inductive and using Fixpoint. What are pros and cons ...
- 224
4
votes
2
answers
153
views
Pragmatic encodings of inductive inductive types
What's the most pragmatic encoding for inductive-inductive types such as for a universe of types?
In pseudo Coq syntax.
...
- 2,868