Los tipos de AFAIU pueden ser Set
cuyos elementos son programas o proposition
cuyos elementos son pruebas. Entonces, en base a este entendimiento:
Inductive prod (X Y: Type) : Set :=
| pair: X -> Y -> prod X Y.
El siguiente código debe compilarse, pero no se debe al siguiente error. Si cambio Set
con Type
u otro Type
con Set
él se compila bien. ¿Alguien puede ayudarme a entender lo que significa el siguiente error? Estoy tratando de enseñarme Coq usando el libro de Fundamentos de Software.
Error:
Error: Large non-propositional inductive types must be in Type.
dependent-types
coq
Abhishek Kumar
fuente
fuente
Respuestas:
Coq tiene 3 tipos "grandes":
Prop
está destinado a proposiciones. Es impredicativo, lo que significa que puede crear instancias de funciones polimórficas con tipos polimórficos. También tiene irrelevancia de prueba, lo que significa que si entonces . Esto permite que los términos que solo se usan para la prueba se borren en cualquier código generado por Coq.Set
está destinado a la computación. Es predicativo y no tiene irrelevancia de prueba, lo que le permite hacer cosas buenas como no suponer . Las partes permanecen durante la extracción del código.Set
Type
es un supertipo de ambos, lo que le permite escribir código una vez que funciona con cualquieraEstoy bastante seguro de que su error se debe a que está definiendo un
Set
cuyos parámetros pueden serType
, lo que significa que pueden serProp
, lo que no está permitido. Si cambia a esto:Tu código debería funcionar.
fuente
Prop
menos que lo agregue como axioma.