Czym różni się zestaw od typu w Coq? [Zamknięte]

Typami AFAIU może być element, Setktórego elementami są programy, lub propositionktórego elementami są dowody. Opierając się na tym zrozumieniu:

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

Poniższy kod powinien się skompilować, ale nie wynika to z następującego błędu. Jeśli zmienię Setz tym Typelub innym Typez Setnim kompiluje się dobrze. Czy ktoś może mi pomóc zrozumieć, co oznacza następujący błąd? Staram się nauczyć Coq za pomocą książki Software Foundations.

Błąd:

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

dependent-types coq

— Abhishek Kumar
źródło

Dowody twierdzeń zawsze były szarą strefą dla CS.SE, ale zgaduję, że jest to dobry kandydat na migrację modów do StackOverflow.

— jmite

To pytanie zawiera kilka odpowiedzi tutaj .

— Anton Trunov

@jmite Biorąc pod uwagę, że to pytanie dotyczy rachunku konstrukcji z Coq służącym tylko jako konkretna składnia, myślę, że jest tutaj na temat.

— Gilles „SO- przestań być zły”

Coq ma 3 „duże” typy:

Prop $p_1, p_2 : P$ $p_1 = p_2$
Set $1 = 2$ Set
Type jest nadtypem obu z nich, co pozwala na napisanie kodu, który będzie działał z każdym z nich

Jestem prawie pewien, że twój błąd wynika z tego, że definiujesz, Setczyje parametry mogą być Type, co oznacza, że mogą być Prop, co jest niedozwolone. Jeśli zmienisz to:

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

twój kod powinien działać.

— jmite
źródło

Coq nie ma dowodu nieistotności, Propchyba że dodasz go jako aksjomat.

— Geoff,