[Agda] Does the order of patterns matter?

[Martin Escardo]

On 27/09/12 13:35, Altenkirch Thorsten wrote:
>>>> Already in definitions by pattern matching on natural
>>>> numbers there is a departure from Martin-Lof type theory, because in
>>>> MLTT you need an inductive definition to even compute the predecessor
>>>> function.
>>>
>>> I don't understand this remark.
>>>
>>> Certainly we can define
>>>
>>> pred : Nat -> Nat
>>> pred 0 = 0
>>> pred (suc n) = n
>>>
>>> without any difficulties.
>>
>> Yes, that's my point. How do you write in MLTT?
>
> What is wrong with
>
> pred : ℕ → ℕ
> pred = RecNat (λ _ → ℕ) 0 (λ n x → n)

There is nothing wrong with it. It just doesn't uses cases, it uses 
recursion. That was the only observation. Anyway, certainly the least 
important observation/question I wanted to make in the previous message.

Martin