[Agda] Reasoning with Pattern Match with Default Cases

[Jesper Cockx]

Ah, I was thinking of the SplitTree data type, which doesn't have default
cases. But you're right that the CompiledClauses type does have them.

cheers,
Jesper

On Thu, Nov 12, 2015 at 10:38 PM, Ulf Norell <ulf.norell at gmail.com> wrote:

>
>
> 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/20151113/49d47961/attachment.html