Чем отличается Set от Type в Coq? [закрыто]

Типы AFAIU могут быть Setэлементами, чьи элементы являются программами, или propositionэлементами, чьи элементы являются доказательствами. Итак, исходя из этого понимания:

Inductive prod (X Y: Type) : Set := 
| pair: X -> Y -> prod X Y.

Следующий код компиляции , но это не из - за следующей ошибки. Если я изменяю Setс Typeили другой Typeс Setним составляет штраф. Может кто-нибудь помочь мне понять, что означает следующая ошибка? Я пытаюсь научить себя Coq, используя книгу Software Foundations.

Ошибка:

Error: Large non-propositional inductive types must be in Type.

Coq имеет 3 "больших" типа:

• Prop$p_1, p_2 : P$$p_1 = p_2$
• Set$1 = 2$Set
• Type является супертипом обоих из них, позволяя вам написать код, который работает с

Я уверен, что ваша ошибка в том, что вы определяете, Setчьи параметры могут быть Type, что означает, что они могут быть Prop, что недопустимо. Если вы измените на это:

Inductive prod (X Y: Set) : Set := 
| pair: X -> Y -> prod X Y. 

ваш код должен работать.