AFAIU types can be a
Set whose elements are programs or a
proposition whose elements are Proofs. So based on this understanding:
Inductive prod (X Y: Type) : Set := | pair: X -> Y -> prod X Y.
Following code should compile but it does not due to the following error. If I change
Type or the other
Set it compiles fine. Can someone help me understand what the following error means? I am trying to teach myself Coq using Software Foundations book.
Error: Large non-propositional inductive types must be in Type.