Buenas,
En la plantilla para el ejercicio 5 puede ser que le falte un parámetro más ?9 al último opK? (y que eso lleve a tener que también que agregar un forall más al lema además del que define los Sets?.
Capaz estoy definiendo mal el tipo de opS, pero al menos como lo estoy definiendo necesito que el último opK tenga un parámetro más que el primero para que los tipos coincidan.
Saludos,
Noelia
Hola Noelia,
No falta un parámetro. Observar que hay tipos que coinciden y en particular ?2 y ?5 son tipos que corresponden a funciones. Una ayudita:
Lemma e52 : forall A B : Set, opS A (B->A) ?3 (opK ?4 (B->A)) (opK ?6 ?7) = opI ?8.
...
Saludos, Carlos
Hola, como puede ser el primer parámetro de opS A si tiene que ser de tipo A -> B -> C según la definición de opS?
Hola.
Definition opS (A B C: Set) (f : A -> B -> C) (g : A -> B) (x : A) := (f x) (g x).
tiene tipo (lo podés ver con Check):
opS : forall A B C : Set, (A -> B -> C) -> (A -> B) -> A -> C
Los tres tipos que tenés que instanciar en el ejercicio para opS corresponden a A, B y C de arriba. Por ejemplo, si instanciaras los tres con un tipo X, el tipo resultante sería:
opS X X X : (X -> X -> X) -> (X -> X) -> X -> X
Saludos, Carlos
