[Agda] Does the order of patterns matter?
Martin Escardo
m.escardo at cs.bham.ac.uk
Thu Sep 27 15:09:45 CEST 2012
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
More information about the Agda
mailing list