[Agda] Termination checker: indirect subterms used in "where" clauses

Guillaume Brunerie guillaume.brunerie at gmail.com
Sat Jun 23 16:54:55 CEST 2012


Hi,
I have the following code

> module Test where
>
> data ℕ : Set where
>   O : ℕ
>   S : ℕ → ℕ
>
> -- Does compile
> g : ℕ → ℕ
> g O = O
> g (S O) = S O
> g (S (S n)) = g (S n)
>
> -- Does not compile
> f : ℕ → ℕ
> f O = O
> f (S O) = S O
> f (S (S n)) = a where
>   a : ℕ
>   a = f (S n)

Why does g compiles and not f (f is highlighted red in emacs)?
Is this a bug or something not yet implemented?
Is there an easy way to work around it?
(I using a dev version of Agda compiled a few weeks ago)

Thanks!

Guillaume


More information about the Agda mailing list