[Agda] Termination Checking

[Andreas Abel]

Hi Leonardo,

That should really terminate, I fixed this in the darcs version of Agda 
now.

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 φ′

This termination checks even in the release version.

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/