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

[Guillaume Brunerie]

Thanks Guillaume, it works :-)
Le 23 juin 2012 17:03, "gallais @ ensl.org" <guillaume.allais at ens-lyon.org>
a écrit :

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120623/d476e918/attachment.html