<div class="gmail_quote">On Wed, Feb 22, 2012 at 9:02 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Why has foo a second argument "Bool" after "true"?<br></blockquote><div><br>I don't know. I'm hoping that was a copy/paste error. <br></div><div> </div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Also, note that the equation<br>
<br>
a = if x then a else a<br>
<br>
does not hold definitionally in Agda. Hence the complaint of Agda.<br></blockquote><div><br>OK, I think that explains it...<br> </div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
That Agda prints y as @0 points to some problem in Agda.<br></blockquote><div><br>Right.<br> </div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
Cheers,<br>
Andreas<div><div class="h5"><br>
<br>
On 22.02.12 9:34 PM, Ramana Kumar wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
Why exactly does this fail?<br>
Should it?<br>
<br>
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>
<br>
which is a little cryptic (but probably no more so than my declaration).<br>
<br>
<br></div></div>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><span class="HOEnZb"><font color="#888888"><br>
</font></span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
-- <br>
Andreas Abel <>< 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/%7Eabel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</font></span></blockquote></div><br>