Hola Gustavo,
el otro dia tenia un par de dudas generales y quede en escribirlas por aca.
Era sobre devolver el tipo X que es Set en lugar de devolver Set.
Por ejemplo, en el ejercicio 8 si defino el ArrayNat general asi:
Parameter Array: forall(X:Set)(n:nat),X.
Luego cuando defino por ejemplo empty_ asi:
Parameter empty_ : foral(X:Set), Array X 0.
no puedo porque el tipo de Array X 0 es X y no Set como debería.
O sea, si cambio la definición de Array a:
Parameter Array : forall (X:Set)(n:nat),Set.
ahí si me deja pero no lo veo correcto.
En cambio si lo hago como "Definition" ahí si me deja que el tipo de Array X 0 sea X en lugar de Set.
Se entiende mi planteo? Y cual seria entonces la forma adecuada de hacerlo, con Definition o con Parameter y como tipo de salida Set en lugar del X?
Gracias, saludos.