[Agda] Does the order of patterns matter?

[Martin Escardo]

On 27/09/12 12:06, Altenkirch Thorsten wrote:
>
>
> On 27/09/2012 11:51, "Martin Escardo" <m.escardo at cs.bham.ac.uk> 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?