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

[Benja Fallenstein]

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).

- Benja