Práctico 3 - Ej 3 parte 4

Práctico 3 - Ej 3 parte 4

de Enzo Fabbiani Perez -
Número de respuestas: 1

Buenas,

Como definición de apply tomé lo siguiente:

Definition apply: (A->B)->A->B := fun f n => (f n).


Luego, para la parte 4 en donde debe ser válido para cualquier conjunto se me ocurrió hacer esto:

Definition apply2: forall A B : Set, (A->B)->A->B :=  fun (X:A)(Y:B)f n => (f n).

Que lo leería como para todo A y B de tipo Set, la función que recibe parámetros X de tipo A e Y de tipo B (que implicitamente ya son de tipo Set por la cuantificación) devuelve f aplicado a n.

Sin embargo Coq me dice Found "A" where "Set" was expected. Si sustituyo A y B por Set anda bien.

Por que pasa esto? Capaz estoy entendiendo algo mal.

Gracias.


En respuesta a Enzo Fabbiani Perez

Re: Práctico 3 - Ej 3 parte 4

de Carlos Luna -

Hola.

El tipo que ponés en apply2 es correcto pero no se corresponde con el término. En particular "(X:A)" debe ser "(A:Set)". El primer argumento de apply2 debe ser un Set no un elemento de tipo Set. Lo mismo para el otro Set (B).

Definition apply2: forall A B : Set, (A->B)->A->B :=  fun (A:Set) (B:Set) f n => f n.

Saludos, Carlos