Buenas,
Muchas Gracias.
Parameter es usado aquí para definir tipos (en particular familias) y constructores de tipo. En el siguiente práctico veremos como definir estos tipos y sus constructores usando definiciones inductivas. Por ahora vemos estos elementos como axiomas (Parameter y Axiom son equivalentes).
En Definition ArrayNat := fun (n:nat) => Set, ArrayNat tiene tipo nat -> Type, mientras que en Parameter ArrayNat : forall n:nat, Set, el tipo de ArrayNat es nat -> Set. Esta última definición nos permite definir un Set paramétrico en los naturales (arreglos de naturales de cierto largo).
En 8.6 Array debería ser paramétrico también en el tipo de los elementos del arreglo:
Parameter Array : forall (A:Set) (n:nat), Set.
Por ejemplo, para agregar elementos tendríamos un add':
Parameter add' : forall (A:Set) (n:nat), A -> Array A n -> Array A (n + 1).
Espero haber aclarado las dudas, sino por favor volvé a escribir.
Para chequear tipos usá el comando Check.
Saludos, Carlos
Me quedó claro, gracias.
Otra duda, en la parte 8.7 hay que utilizar el tipo bool estandar de coq no? Es decir, no el tipo Bool que definimos en el ejercicio 7.
Muchas gracias.
El tipo bool de Coq.
