[Agda] Does the order of patterns matter?

[Nils Anders Danielsson]

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"):

   http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.PatternMatching

-- 
/NAD