Awesome!<br><br><div class="gmail_quote">On Wed, Feb 22, 2012 at 10:47 PM, Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

Fixed.  Now it prints as y.<div class="im"><br>
<br>
On 22.02.12 10:05 PM, Ramana Kumar wrote:<br>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
    That Agda prints y as @0 points to some problem in Agda.<br>
<br>
<br>
Right.<br></div><div class="im">
        data foo : (y : Bool) → if y then Set else Set where<br>
           bar : foo true Bool<br>
<br>
        The error I get is<br>
<br>
        if @0 then Set else Set != Set of type Set₁<br>
        when checking the definition of foo<br>
</div></blockquote>
<br><div class="HOEnZb"><div class="h5">
<br>
-- <br>
Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</div></div></blockquote></div><br>