[Agda] Does the order of patterns matter?

Nils Anders Danielsson nad at chalmers.se
Wed Sep 26 13:11:36 CEST 2012

On 2012-09-26 12:51, Achim Jung wrote:
>     I am new to Agda and have run into the following problem. When
> defining a term by pattern matching and when those patterns are
> mutually exclusive, then it seems to me that the order in which they
> are listed should not matter. However, while trying to prove a simple
> statement about equality modulo 2 on the natural numbers, I discovered
> a case where it appears to matter a lot, in that for the first
> definition my theorem type-checks whereas for the second it doesn't.
> The attached short Agda code file is very simple and hopefully
> self-explanatory.

Your issue is discussed on the following page (under the heading
"Reduction behavior"):



More information about the Agda mailing list