[Agda] Re: This ain't right, is it?

[Ulf Norell]

On Sat, Oct 31, 2009 at 2:05 AM, Benja Fallenstein <
benja.fallenstein at gmail.com> wrote:

> On Sat, Oct 31, 2009 at 12:54 AM, Benja Fallenstein
> <benja.fallenstein at gmail.com> wrote:
> > The following type-checks with the darcs version of Agda (and
> > --universe-polymorphism):
> >
> > IsThatRight : {i : Level} → Set i
> > IsThatRight {i} = (R : Set i) → R
>
> Surprisingly, this does not type-check any longer when I add a
> LEVELMAX pragma (I only defined LEVEL, LEVELZERO and LEVELSUC before).
>

That is clearly a bug. Can you add your example to this issue:

http://code.google.com/p/agda/issues/detail?id=203

Thanks, Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091031/a4e60351/attachment.html