Hi again, (sorry about the blank reply a second ago)
You are on the right track, the correct statement of the oh2 constructor
would look like this, however:
a : A
-----------------------------
oh2 a : So2 (Just a)
You can't say 'justA : (Just a)' because 'Just a' is not a type. Luckily you
can do the indexing directly, as show above.
Hope this helps,
Peter
On 04/03/2008, Peter Morris <[EMAIL PROTECTED]> wrote:
>
>
>
> 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.
> >
>
>
