Táctica refine

Táctica refine

de Juan Pablo Sierra Ansuas -
Número de respuestas: 2

Bueno, estoy meta darle vueltas al asunto pero no me logro dar cuenta cómo es que hay que usar esta táctica. En internet hay unos ejemplos que no logro comprender muy bien y termina pareciendo medio mágico. Veo que en muchos casos le ponen un fun x => algo adentro del paréntesis.

No logro entender bien cómo es que hay que engancharlo con lo que se quiere demostrar, siempre me salta un error de tipos. Además, me gustaría entender bien cuando es que se usa _ y como es el tema del match adentro del refine.

Por último, me serviría pila si alguien me pudiera tirar algún ejemplo entendible.

Gracias !

En respuesta a Juan Pablo Sierra Ansuas

Re: Táctica refine

de Carlos Luna -

Hola.

Esta táctica no se usa (no se precisa usar en el práctico); no se si la comentaron en el teórico.

Hay información (y un ejemplo) en:

https://coq.inria.fr/distrib/current/refman/Reference-Manual011.html#@default513.

Puede usarse para dar un término de prueba (típicamente una función) incompleto (usando _); que luego será refinado. Con un exact uno tiene que dar exactamente el término de prueba.

Saludos, Carlos