[Agda] Termination checker: indirect subterms used in "where"
clauses
gallais at ensl.org
guillaume.allais at ens-lyon.org
Sat Jun 23 17:03:05 CEST 2012
Hi Guillaume,
you can ask agda to do more work during termination analysis
with the appropriate pragma. Cf the release notes for 2.2.8 [1]
(ctrl+f termination-depth to find quickly the interesting bits)
Using {-# OPTIONS --termination-depth=2 #-} solves your problem.
Cheers,
--
gallais
[1] http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-8
On 23 June 2012 15:54, Guillaume Brunerie <guillaume.brunerie at gmail.com> wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list