<br><div class="gmail_quote">On Sat, Oct 31, 2009 at 2:05 AM, Benja Fallenstein <span dir="ltr"><<a href="mailto:benja.fallenstein@gmail.com">benja.fallenstein@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div class="im">On Sat, Oct 31, 2009 at 12:54 AM, Benja Fallenstein<br>
<<a href="mailto:benja.fallenstein@gmail.com">benja.fallenstein@gmail.com</a>> wrote:<br>
> The following type-checks with the darcs version of Agda (and<br>
> --universe-polymorphism):<br>
><br>
> IsThatRight : {i : Level} → Set i<br>
> IsThatRight {i} = (R : Set i) → R<br>
<br>
</div>Surprisingly, this does not type-check any longer when I add a<br>
LEVELMAX pragma (I only defined LEVEL, LEVELZERO and LEVELSUC before).<br></blockquote><div><br>That is clearly a bug. Can you add your example to this issue:<br><br><a href="http://code.google.com/p/agda/issues/detail?id=203">http://code.google.com/p/agda/issues/detail?id=203</a><br>
<br>Thanks, Ulf<br></div></div><br>