<div dir="ltr"><div><div>Ah, I was thinking of the SplitTree data type, which doesn't have default cases. But you'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"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></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"><<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>></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't have any default cases, this would have the effect that default cases aren'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>