[Agda] Changing import lists turns constructors into variables

Ulf Norell ulf.norell at gmail.com
Tue Mar 3 17:54:24 CET 2009


On Wed, Feb 25, 2009 at 8:32 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk>wrote:

>
> 4) Thorsten noted that this particular instance of the problem could
>  have been avoided if Agda had warned about unreachable patterns.
>
> I'm leaning towards 4). Hopefully it is easy to change the coverage
> checker so that it complains if only a proper subset of the clauses is
> needed to reach full coverage. Ulf?
>

Yup, not very hard. Implemented now.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090303/3324c1de/attachment.html


More information about the Agda mailing list