<br><div class="gmail_quote">On Sat, Oct 31, 2009 at 2:05 AM, Benja Fallenstein <span dir="ltr">&lt;<a href="mailto:benja.fallenstein@gmail.com">benja.fallenstein@gmail.com</a>&gt;</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>
&lt;<a href="mailto:benja.fallenstein@gmail.com">benja.fallenstein@gmail.com</a>&gt; wrote:<br>
&gt; The following type-checks with the darcs version of Agda (and<br>
&gt; --universe-polymorphism):<br>
&gt;<br>
&gt; IsThatRight : {i : Level} → Set i<br>
&gt; 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>