Buenas
No me queda del todo claro por que ArrayNat es un array de naturales.
Entiendo que el tipo es "forall n:nat, Set" y que ahi se menciona un n de tipo nat, pero de las operaciones me parecio que ese era el tamaño del array. De repente por ahi va mi error.
En respuesta a Santiago Puppo Caubarrere
Re: [Practico 3] Ejercicio 8 - Duda ArrayNat
de Carlos Luna -
Hola.
Ese n es el tamaño del arreglo y no el tipo de los elementos.
El tipo de los elementos se precisa al agregar elementos (abajo en negrita):
Parameter add : forall n:nat, nat -> ArrayNat n -> ArrayNat (n + 1).
Saludos, Carlos