Typami AFAIU może być element, Set
którego elementami są programy, lub proposition
któ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ę Set
z tym Type
lub innym Type
z Set
nim 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
źródło
Odpowiedzi:
Coq ma 3 „duże” typy:
Prop
Set
Set
Type
jest nadtypem obu z nich, co pozwala na napisanie kodu, który będzie działał z każdym z nichJestem prawie pewien, że twój błąd wynika z tego, że definiujesz,
Set
czyje parametry mogą byćType
, co oznacza, że mogą byćProp
, co jest niedozwolone. Jeśli zmienisz to:twój kod powinien działać.
źródło
Prop
chyba że dodasz go jako aksjomat.