[Práctico 6] - Ejercicio 6

[Práctico 6] - Ejercicio 6

de Juan Pablo Garcia Garland -
Número de respuestas: 3

Hola.

No me queda claro cual es el objetivo de este ejercicio.

La idea es definir una función que implemente el algoritmo dado y usarla de witness para demostrar nat_div_mod?

O el objetivo es demostrar nat_div_mod a fuerza de tácticas, siguiendo la lógica del algoritmo y luego extraer?

Saludos.

En respuesta a Juan Pablo Garcia Garland

Re: [Práctico 6] - Ejercicio 6

de Carlos Luna -

Hola.

La segunda opción es la indicada.

Saludos, Carlos

En respuesta a Carlos Luna

Re: [Práctico 6] - Ejercicio 6

de Jairo Yamil Bonanata Silva -

Hola, ¿La idea para resolver este ejercicio es definir la función divmod como un Function divmod y luego hacer un exists con eso?
¿Donde puedo leer bien qué hacen los módulos que hay que importar?

Saludos,
Jairo.

En respuesta a Jairo Yamil Bonanata Silva

Re: [Práctico 6] - Ejercicio 6

de Carlos Luna -

Hola Jairo.

En otro mail ya se comentó esto. La idea es seguir la lógica de la función utilizando tácticas.

El contenido de las librerías/bibliotecas puede consultarse en:

https://coq.inria.fr/distrib/current/stdlib/.

Saludos, Carlos