[Agda] Does the order of patterns matter?

[Dan Licata]

On Sep27, Martin Escardo wrote:
> Nils' message tells us where to find a full explanation of what is going 
> on.
>
> On 27/09/12 11:27, Altenkirch Thorsten wrote:
>> The bug is rather that we use the = sign here -
>> Epigram avoided this by using |-> and it also kept track of the 
>> splittings.
>
> But "|->" would also be wrong, because e.g. in Achim's example, there is a 
> situation f lhs = rhs where there is no reduction f lhs |-> rhs. But this 
> is just a notational discussion
>
>
> Here are some questions/conjectures.
>
> (1) It would be possible to implement Agda so that each equation in a 
> pattern holds definitionally, if we wished, I believe. Of course, you would 
> get new definitional equalities not present in Martin-Loef type theory. But 
> does that matter? Conjecture: no new propositional equalities arise.

If I understand you correctly, this doesn't seem quite right, because
you can have overlapping patterns, with a first-match semantics.  E.g.

  eq : Nat -> Nat -> Bool
  eq Z Z = True
  eq (S n) (S m) = eq n m
  eq _ _ = False

Taken in isolution, both the first and third lines match Z Z, but you
clearly can't have both as equations.

-Dan