[Agda] Termination Checking

[Leonardo Rodriguez]

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

> Hi Leonardo,
>
> That should really terminate, I fixed this in the darcs version of Agda
> now.
>
> Thank you :D

>
> On 19.04.11 8:12 PM, Leonardo Rodriguez wrote:
>
>> 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 (φ′ ⇨ φ″)
>>
>
> What you can also do is an overlapping clause here:
>
> bad (φ ⇨ φ′)  = bad φ′
>
>
The "bad" function is an example for reveal the problem. I had this problem
with another
function where i can't overlap clauses.



> This termination checks even in the release version.
>
> Thank you again :D

> Cheers,
> Andreas
>
>
> --
> 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/ce86efe0/attachment.html