[Agda] Termination checker and rewriting

[Jesper Cockx]

>
> On 29/01/2019 13.57, Guillaume GENESTIER wrote:
> > More specifically, I was wondering if any termination checking is
> > performed on these rules.
>
> No.


... but if you are interested in working on implementing a termination
checker for rewrite rules, send me a mail and let's talk.

-- Jesper

On Tue, Jan 29, 2019 at 2:19 PM Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 29/01/2019 13.57, Guillaume GENESTIER wrote:
> > More specifically, I was wondering if any termination checking is
> > performed on these rules.
>
> No.
>
> --
> /NAD
> _______________________________________________
> 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/20190129/e1d1705a/attachment.html>