<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">&lt;<a moz-do-not-send="true"
                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'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>