[Práctico 4] Ejercicio 7

[Práctico 4] Ejercicio 7

de Eliana Rosselli Orrico -
Número de respuestas: 2

Buenas, 

Me surgió una duda realizando algunos ejercicios del práctico, por ejemplo en el ejercicio 7. No entendía mucho cómo definir el tipo Exp y buscando en el foro encontré este hilo https://eva.fing.edu.uy/mod/forum/discuss.php?d=73173 que lo explica. 

La duda que me surgió es que en realidad si uso el código de la función val tal cual como está en el post, coq me da un error en la linea de id a => a, 

Error: The constructor id (in type Exp) expects 2 arguments.

Intenté entonces pasarle el tipo nat, es decir id nat a => a, y ahí me da un error diferente. 

Error: The parameters do not bind in patterns; they must be replaced by '_'.

Entiendo que debo pasarle _ en vez del tipo para que compile, pero no entiendo por qué no puedo pasarle explícitamente un tipo en el pattern del match. 

Gracias y saludos

En respuesta a Eliana Rosselli Orrico

Re: [Práctico 4] Ejercicio 7

de Carlos Luna -

Hola Eliana.

Si ver bien tus definiciones te digo que parece ser un tema de la versión de Coq, que va cambiando (el post que referís es de 2015).

Si ponés: Set Implicit Arguments, Coq deduce a partir de ahí el argumento del tipo y directamente lo omitís: id a => a. Pero sino, tenés que poner _ en el tipo de los elementos cuando hacés un match de un elemento de tipo Exp (no acepta nat en este caso).

Saludos, Carlos