[Agda] Termination Checking

[Leonardo Rodriguez]

module Test where
open import Data.Nat

infixr 3 _⇨_
data Type : Set where
 int   : Type
 _⇨_   : Type → Type → Type

bad : Type → ℕ
bad int = 0
bad (φ ⇨ int) = bad φ
bad (φ ⇨ (φ′ ⇨ φ″))  = bad (φ′ ⇨ φ″)

ok : Type → ℕ
ok int = 0
ok (φ ⇨ φ′) with φ′
... | int = ok φ
... | (φ″ ⇨ φ‴) = ok (φ″ ⇨ φ‴)

The problem is that function "bad" fails on termination checking. But the
function "ok" is a rewrite of "bad" that terminates.
Thanks.
Leo

2011/4/19 Andreas Abel <andreas.abel at ifi.lmu.de>

> Can't see why I should not terminate.  Can you provide a self-contained
> Agda-loadable version of your example?
>
> Thanks
> Andreas
>
>
> On 19.04.11 1:27 AM, Leonardo Rodriguez wrote:
>
>> Hi,
>>
>> This is a very simple function that fails on termination checking:
>> http://pastebin.com/WDtSPxqq
>> why ? Any hint will be appreciated
>> thanks you in advance
>>
>> Leo
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110419/f5a9156d/attachment.html