Buenas,
Me surgió una duda sobre el ejercicio 8 del práctico 3. No me queda claro qué es bien la keyword Parameter. Es como que únicamente se están definiendo los tipos de add, ArrayNat, etc. pero no su implementación? En los ejercicios que debemos definir los parámetros concat, zip, etc, la idea es solo definir su tipo?
En la parte 7 del ejercicio tenemos que definir ArrayBool para vectores de booleanos. La idea es usar el tipo Bool definido en el ejercicio 7?
Gracias y saludos
Eliana
Hola.
Parameter permite definir objetos de ciertos tipos, como axiomas esencialmente. Tal como vos decís, se está definiendo el tipo de add (y no su implementación) en:
Parameter add : forall n : nat, nat -> ArrayNat n -> ArrayNat (S n).
Respecto a "En los ejercicios que debemos definir los parámetros concat, zip, etc, la idea es solo definir su tipo?": SI. Por ejemplo:
Parameter concat : forall n m : nat, ArrayNat n -> ArrayNat m -> ArrayNat (n + m).
Respecto a tu última consulta de la parte 7, usá el tipo "bool" predefinido de Coq.
Saludos, Carlos
