[Agda] Does the order of patterns matter?

[Martin Escardo]

I think we were talking about mutually exclusive patters, Dan. Martin

On 27/09/12 14:45, Dan Licata wrote:
> 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
>