[Agda] Does the order of patterns matter?

[Martin Escardo]

On 26/09/12 12:04, Altenkirch Thorsten wrote:
> basically a pattern in Agda is a proof of exhaustiveness and Agda will
> only recognize exhaustive patterns which are produced by splitting a
> trivial pattern.

But the patterns are recognized as exhaustive in the given example.

The relations ≡ and ≡' (both meaning equality modulo 2, not equality) 
have the same definitions, except that the order of the equations are 
different. Because they are mutually exclusive, this shouldn't matter.

Now, this type-checks:

thm : ∀(x y : ℕ) → (x ≡ y) → (succ x ≡ succ y)
thm x y p = p

But this doesn't:

no-thm : ∀(x y : ℕ) → (x ≡' y) → (succ x ≡' succ y)
no-thm x y p = p

Why???

Martin