Buenas,
Intentando resolver el ejercicio 1 llegue a dos posibles soluciones y no me doy cuenta si son exactamente lo mismo o si hay alguna diferencia que no estoy notando.
Por ejemplo:
Considerando el tipo: (A->A)->(A->A)-> A -> A
Las posibles soluciones a las que llego son:
Definition test1 : (A->A)->(A->A)-> A -> A := fun f => fun g => fun x => f (g x).
Definition test2 (f: A -> A) (g : A -> A) (x : A) := f (g x).
En test1 puse el tipo al que pedían encontrar un elemento y lo resolví pensando que era λf.λg.λx.f(g x) y remplazando λ por fun y . por =>.
En test2 directamente dije de que tipo era cada elemento sin usar fun ni =>.
Si no son lo mismo, ¿Cuál es la solución esperada?
Saludos.