[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