[Agda] Does the order of patterns matter?

Martin Escardo m.escardo at cs.bham.ac.uk
Wed Sep 26 13:13:13 CEST 2012

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



More information about the Agda mailing list