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
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