[Agda] Does the order of patterns matter?

[Achim Jung]

Hello,

    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.

    Achim.

PS: I am running version 2.3.0.1 on Ubuntu 12.04.

-------------------------------------------------------------------------
  Prof Achim Jung			Tel.: (+44) 121 41 44776
  School of Computer Science		Sec.: (+44) 121 41 42791
  The University of Birmingham		Fax.: (+44) 121 41 44281
  Edgbaston				Email: A.Jung at cs.bham.ac.uk
  BIRMINGHAM, B15 2TT			Web: http://www.cs.bham.ac.uk/~axj
  England
-------------------------------------------------------------------------
-------------- next part --------------
-----------------------------------------------------
-- Author: Achim Jung (A.Jung at cs.bham.ac.uk)
-- Date: 25 September 2012
-----------------------------------------------------
module Mod2 where

data ??? : Set where
 zero : ???
 succ : ??? ??? ???

data ??? : Set where

data ??? : Set where
 * : ???

-- Equality modulo 2; first version
_???_ : ??? ??? ??? ??? Set
-- Here, this pattern is listed first --
succ x ??? succ y         = x ??? y 
----------------------------------------
zero ??? zero             = ???
zero ??? succ zero        = ???
zero ??? succ (succ y)    = zero ??? y
succ zero ??? zero        = ???
succ (succ x) ??? zero    = x ??? zero
infixl 4 _???_

thm : ???(x y : ???) ??? (x ??? y) ??? (succ x ??? succ y)
thm x y p = p

-- Equality modulo 2; second version
_???'_ : ??? ??? ??? ??? Set
zero ???' zero             = ???
zero ???' succ zero        = ???
zero ???' succ (succ y)    = zero ???' y
succ zero ???' zero        = ???
succ (succ x) ???' zero    = x ???' zero
-- Here it is listed last --------------
succ x ???' succ y         = x ???' y 
----------------------------------------
infixl 4 _???'_

no-thm : ???(x y : ???) ??? (x ???' y) ??? (succ x ???' succ y)
no-thm x y p = p