[CST-2] Types

[Shu Yan Chan]

Thanks for your reply, but I still don;t fully understand your solution:

> Looking at it now, I'm not
> entirely sure about whether the \v:g is in the right place, but I'll leave
> it as it is and see if anyone corrects it!

> Compose_g_d_e = \f:g->Opt_d, g:d->Opt_e ( \v:g (

I guess it should be \v:d  ?

>                      /\a' (\x':a', f':e->a' (
>                      (f v) a' x' (\v':d (
>                      (g v') a' x' (\v'':e (f' v''))

I think replacing (\v'':e (f' v'')) with f' directly would do the same job?
since (f v) is of type Opt d, (\v':d ((g v') a' x'   f' ) is of type d ->a'
!!???
so (f v) a' x' (\v':d ( (g v') a' x'    f' ) is of type a' ???

>                      )))

Thanks,

Yours,
Shu Yan