Hola, no estoy seguro de si lo estoy haciendo bien.
Se que pidieron que no mandemos código pero preciso que me verifiquen si están bien estos 2 ejemplos para saber si lo estoy entendiendo bien. COQ me dice que están bien, pero el tema es que no estoy seguro si los estoy escribiendo bien en COQ.
Section Ejercicio2.
Variable A B C: Set.
(* [x:?][y:?][z:?]((x y)z) *)
Definition term_3_2_1 := fun (x: A -> B -> C) (y: A) (z: B) => x y z.
Check term_3_2_1. (* (A -> B -> C) -> A -> B -> C *)
(* [x:?][y:?][z:?](x (y z)) *)
Definition term_3_2_2 := fun (x: B -> C) (y: A -> B) (z: A) => x (y z).
Check term_3_2_2. (* (B -> C) -> (A -> B) -> A -> C *)
End Ejercicio2.
Y con este
Que notación es esta? Yo pensaba que era lo mismo que λz.λx.λy((x y) z) pero con los paréntesis curvos me descoloco.
Saludos