[Agda] termination with `where'

[Andreas Abel]

Yes, this is a bit unsatisfactory, but Agda treats a `where` definition 
as a mutually recursive function, and the termination checker does not 
unfold `where` definitions.

In you case you should be able to use `let` instead, which is just a 
substitution.

   ... let z = e :* e'
       in ...  aux x z ...

Best,
Andreas

On 02.06.2017 21:16, Sergei Meshveliani wrote:
> Dear Agda developers,
> 
> For a certain fragment of
> 
>    f : (u v : Expression) -> foo u v ≈ foo' u v
>    f (x :+ y) (e :* e') =
>      begin
>       ...    ≈[ +cong (aux x z)
>                       (aux y z)   -- (I)
>               ]
>       ...
>      ∎
>      where z = e :* e'
> 
> Agda 2.6.0-207bde6  reports  "Termination checking failed ...",
> and marks yellow the call  (aux y z).
> 
> Replacing  (aux y z)  with   (aux y (e :* e'))
> satisfies the type checker.
> Here  x, y, e, e'  are terms constructed with certain data
> constructors  :0, :1, gen, _:+_, _:*_.
> 
> It looks strange that the termination checker is not stable under the
> `where' construct.
> 
> What people think of this?
> 
> Regards,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/