<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">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><div>Actually, the case tree representation we use does have default cases.</div><div><br></div><div>/ Ulf</div></div></div></div>