[Practico 3][Ejercicio 8.2]

[Practico 3][Ejercicio 8.2]

de Agustin Di Vincezo Fernandez -
Número de respuestas: 2

Buenas,

Quería consultar ya que no estoy seguro de lo que estoy haciendo. 

Primero, mi solución fue utilizar Check y escribir el termino que representa el vector pedido (como en el ejercicio 8.1), eso es lo esperado?

Segundo, en cada "invocación" del add, es correcto escribir (0+1+..1) en el primer parámetro, o se debería escribir de otra forma? haciendo esto, lo que obtengo del check por ejemplo para el array de largo 4: : ArrayNat (0 + 1 + 1 + 1 + 1), eso es lo esperado?


Gracias

Saludos

En respuesta a Agustin Di Vincezo Fernandez

Re: [Practico 3][Ejercicio 8.2]

de Carlos Luna -

Hola!

Si, está bien. Por ejempo:

Definition vector_00 := add 1 0 (add 0 0 empty).

Check vector_00. (* acá poné ArrayNat (1 + 1) *)

Ver la alternativa: Check vector_00 : ArrayNat 2.

En cada invocación de add podés poner el nat correspondiente, si querés. Por ejemplo:

Definition vector_0101 := add 3 1 (add 2 0 (add 1 1 (add 0 0 empty))).

Check vector_0101 : ArrayNat 4.

Saludos, Carlos