[Agda] Reasoning with Pattern Match with Default Cases

[Aaron Stump]

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.
Aaron

On 11/12/2015 03:38 PM, Ulf Norell wrote:
>
>
> On Thu, Nov 12, 2015 at 8:59 PM, Jesper Cockx <Jesper at sikanda.be 
> <mailto:Jesper at sikanda.be>> wrote:
>
>     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.
>
>
> Actually, the case tree representation we use does have default cases.
>
> / Ulf
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151112/054a7f49/attachment.html