# [Agda] Does the order of patterns matter?

Achim Jung A.Jung at cs.bham.ac.uk
Wed Sep 26 12:51:16 CEST 2012

```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

```