On 04/03/2008, Serguey Zefirov <[EMAIL PROTECTED]> wrote:
>
> Being not satisfied with solution I spun from thin air I decided to
> reimplement it once again.
>
> If I could invent a type So2 indexed by (Maybe a) type, I could get
> the following more appropriate definitions of wNil and wCons (Haskell
> style):
> wNil = W Nothing notSo2
> wCons a as = W (Just a) (lam p => as)
>
> But I cannot get a type, indexed by Maybe:
> ( A : * ; a : Maybe A ! ( a : A ; justA : (Just a) !
> data !----------------------! where !---------------------------!
> ! So2 a : * ) ! oh2 : So2 justA )
>
> Epigram colors a whole definition in light brown and (Just a) in an
> even more brown color. I think it tells me that I am wrong, but I
> cannot understand why.
>
> Again.
>
