[Agda] Reasoning with Pattern Match with Default Cases

[Ulf Norell]

On Thu, Nov 12, 2015 at 8:59 PM, Jesper Cockx <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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151112/0adbd847/attachment.html