[Agda] Changing import lists turns constructors into variables

Remi Turk rturk at science.uva.nl
Thu Feb 26 01:15:48 CET 2009


On Wed, Feb 25, 2009 at 07:32:46PM +0000, Nils Anders Danielsson 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?

Any idea how easy it would be to also make it warn about
pattern variables having the same name as a non-imported
constructor of the same type?

Cheers, Remi


More information about the Agda mailing list