<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
I ran into this issue, too. It would be interesting if Agda could
keep track of the fact that certain patterns had not matched a given
term -- but maybe not worth the additional complexity in theory and
implementation.<br>
Aaron<br>
<br>
<div class="moz-cite-prefix">On 11/12/2015 03:38 PM, Ulf Norell
wrote:<br>
</div>
<blockquote
cite="mid:CAJjNqYGYvGzoLhSMHX8xdMcU=azQfekwW1BmF8DMXaNU+DmKYw@mail.gmail.com"
type="cite">
<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"><<a moz-do-not-send="true"
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>
<div>Actually, the case tree representation we use does have
default cases.</div>
<div><br>
</div>
<div>/ Ulf</div>
</div>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>