<div dir="ltr"><div><div>Ah, I was thinking of the SplitTree data type, which doesn&#39;t have default cases. But you&#39;re right that the CompiledClauses type does have them.<br><br></div>cheers,<br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 12, 2015 at 10:38 PM, Ulf Norell <span dir="ltr">&lt;<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote"><span class="">On Thu, Nov 12, 2015 at 8:59 PM, Jesper Cockx <span dir="ltr">&lt;<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div>A way to improve how Agda handles these cases would be to do coverage checking before type checking and only type checking the resulting case tree. Since case trees don&#39;t have any default cases, this would have the effect that default cases aren&#39;t typechecked themselves, but only their expanded versions.</div></div></div></div></div></blockquote><div><br></div></span><div>Actually, the case tree representation we use does have default cases.</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>/ Ulf</div></font></span></div></div></div>
</blockquote></div><br></div>